mirror of
https://github.com/AdaCore/why3.git
synced 2026-02-12 12:34:55 -08:00
4609 lines
205 KiB
Plaintext
4609 lines
205 KiB
Plaintext
module Types
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
type nl_fo_formula 'b0 'b1 =
|
|
| NL_Forall (nl_fo_formula 'b0 'b1)
|
|
| NL_Exists (nl_fo_formula 'b0 'b1)
|
|
| NL_And (nl_fo_formula 'b0 'b1) (nl_fo_formula 'b0 'b1)
|
|
| NL_Or (nl_fo_formula 'b0 'b1) (nl_fo_formula 'b0 'b1)
|
|
| NL_Not (nl_fo_formula 'b0 'b1)
|
|
| NL_FTrue
|
|
| NL_FFalse
|
|
| NL_PApp (nl_symbol 'b0) (nl_fo_term_list 'b0 'b1)
|
|
|
|
|
|
type nlimpl_fo_formula =
|
|
{ nlrepr_fo_formula_field : nl_fo_formula int int ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field : int ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field : int ;
|
|
ghost model_fo_formula_field : fo_formula int int ;
|
|
}
|
|
|
|
type cons_fo_formula = | NLC_Forall (int) (nlimpl_fo_formula)
|
|
| NLC_Exists (int) (nlimpl_fo_formula)
|
|
| NLC_And (nlimpl_fo_formula) (nlimpl_fo_formula)
|
|
| NLC_Or (nlimpl_fo_formula) (nlimpl_fo_formula)
|
|
| NLC_Not (nlimpl_fo_formula) | NLC_FTrue | NLC_FFalse
|
|
| NLC_PApp (nlimpl_symbol) (nlimpl_fo_term_list)
|
|
|
|
|
|
end
|
|
|
|
module Logic
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
use Types
|
|
function nat_nlsize_fo_formula (t:nl_fo_formula 'b0 'b1) : nat =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_formula v0) s in s
|
|
| NL_Exists v0 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_formula v0) s in s
|
|
| NL_And v0 v1 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_formula v1) s in
|
|
let s = add_nat (nat_nlsize_fo_formula v0) s in s
|
|
| NL_Or v0 v1 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_formula v1) s in
|
|
let s = add_nat (nat_nlsize_fo_formula v0) s in s
|
|
| NL_Not v0 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_formula v0) s in s
|
|
| NL_FTrue -> let s = one_nat in s | NL_FFalse -> let s = one_nat in s
|
|
| NL_PApp v0 v1 ->
|
|
let s = one_nat in let s = add_nat (nat_nlsize_fo_term_list v1) s in
|
|
let s = add_nat (nat_nlsize_symbol v0) s in s
|
|
end
|
|
|
|
with nlsize_fo_formula (t:nl_fo_formula 'b0 'b1) : int =
|
|
match t with
|
|
| NL_Forall v0 -> let s = 1 in let s = nlsize_fo_formula v0 + s in s
|
|
| NL_Exists v0 -> let s = 1 in let s = nlsize_fo_formula v0 + s in s
|
|
| NL_And v0 v1 ->
|
|
let s = 1 in let s = nlsize_fo_formula v1 + s in
|
|
let s = nlsize_fo_formula v0 + s in s
|
|
| NL_Or v0 v1 ->
|
|
let s = 1 in let s = nlsize_fo_formula v1 + s in
|
|
let s = nlsize_fo_formula v0 + s in s
|
|
| NL_Not v0 -> let s = 1 in let s = nlsize_fo_formula v0 + s in s
|
|
| NL_FTrue -> let s = 1 in s | NL_FFalse -> let s = 1 in s
|
|
| NL_PApp v0 v1 ->
|
|
let s = 1 in let s = nlsize_fo_term_list v1 + s in
|
|
let s = nlsize_symbol v0 + s in s
|
|
end
|
|
|
|
let rec lemma nlsize_positive_lemma_fo_formula (t:nl_fo_formula 'b0 'b1) :
|
|
unit ensures { nlsize_fo_formula t > 0 }
|
|
variant { nat_to_int (nat_nlsize_fo_formula t) } =
|
|
match t with | NL_Forall v0 -> nlsize_positive_lemma_fo_formula v0 ; ()
|
|
| NL_Exists v0 -> nlsize_positive_lemma_fo_formula v0 ; ()
|
|
| NL_And v0 v1 ->
|
|
nlsize_positive_lemma_fo_formula v0 ;
|
|
nlsize_positive_lemma_fo_formula v1 ; ()
|
|
| NL_Or v0 v1 ->
|
|
nlsize_positive_lemma_fo_formula v0 ;
|
|
nlsize_positive_lemma_fo_formula v1 ; ()
|
|
| NL_Not v0 -> nlsize_positive_lemma_fo_formula v0 ; ()
|
|
| NL_FTrue -> () | NL_FFalse -> ()
|
|
| NL_PApp v0 v1 ->
|
|
nlsize_positive_lemma_symbol v0 ;
|
|
nlsize_positive_lemma_fo_term_list v1 ; ()
|
|
end
|
|
|
|
function nlmodel_fo_formula (t:nl_fo_formula 'b0 'b1)
|
|
(fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
|
|
(fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1)) :
|
|
fo_formula 'c0 'c1 =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
Forall
|
|
(nlmodel_fo_formula v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity)))
|
|
| NL_Exists v0 ->
|
|
Exists
|
|
(nlmodel_fo_formula v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity)))
|
|
| NL_And v0 v1 ->
|
|
And
|
|
(nlmodel_fo_formula v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(nlmodel_fo_formula v1 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Or v0 v1 ->
|
|
Or
|
|
(nlmodel_fo_formula v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(nlmodel_fo_formula v1 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Not v0 ->
|
|
Not
|
|
(nlmodel_fo_formula v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_FTrue -> FTrue | NL_FFalse -> FFalse
|
|
| NL_PApp v0 v1 ->
|
|
PApp
|
|
(nlmodel_symbol v0 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity)))
|
|
(nlmodel_fo_term_list v1 ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
let rec lemma nlmodel_subst_commutation_lemma_fo_formula
|
|
(t:nl_fo_formula 'b0 'b1) (fr0:'b0 -> (symbol 'c0))
|
|
(bnd0: int -> (symbol 'c0)) (s0:'c0 -> (symbol 'd0))
|
|
(fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1))
|
|
(s1:'c1 -> (fo_term 'd0 'd1)) : unit
|
|
ensures {
|
|
nlmodel_fo_formula t (subst_compose_symbol fr0 s0)
|
|
(subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr1 s0 s1)
|
|
(subst_compose_fo_term bnd1 s0 s1)
|
|
= subst_fo_formula (nlmodel_fo_formula t fr0 bnd0 fr1 bnd1) s0 s1 }
|
|
variant { nlsize_fo_formula t } =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
nlmodel_subst_commutation_lemma_fo_formula v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity (compose some identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
(compose some identity))
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term (shiftb_fo_term bnd1) identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity))
|
|
=
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term (subst_compose_fo_term bnd1 s0 s1)) identity
|
|
identity)
|
|
} ;
|
|
()
|
|
| NL_Exists v0 ->
|
|
nlmodel_subst_commutation_lemma_fo_formula v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity (compose some identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
(compose some identity))
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term (shiftb_fo_term bnd1) identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term (olifts_fo_term s1) identity identity))
|
|
=
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term (subst_compose_fo_term bnd1 s0 s1)) identity
|
|
identity)
|
|
} ;
|
|
()
|
|
| NL_And v0 v1 ->
|
|
nlmodel_subst_commutation_lemma_fo_formula v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
nlmodel_subst_commutation_lemma_fo_formula v1
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
()
|
|
| NL_Or v0 v1 ->
|
|
nlmodel_subst_commutation_lemma_fo_formula v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
nlmodel_subst_commutation_lemma_fo_formula v1
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
()
|
|
| NL_Not v0 ->
|
|
nlmodel_subst_commutation_lemma_fo_formula v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
()
|
|
| NL_FTrue -> () | NL_FFalse -> ()
|
|
| NL_PApp v0 v1 ->
|
|
nlmodel_subst_commutation_lemma_symbol v0
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
nlmodel_subst_commutation_lemma_fo_term_list v1
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity))
|
|
((rename_subst_fo_term s1 identity identity)) ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol fr0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol fr0 s0) identity) } ;
|
|
assert {
|
|
subst_compose_symbol (rename_subst_symbol bnd0 identity)
|
|
((rename_subst_symbol s0 identity))
|
|
= (rename_subst_symbol (subst_compose_symbol bnd0 s0) identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term fr1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term fr1 s0 s1) identity
|
|
identity)
|
|
} ;
|
|
assert {
|
|
subst_compose_fo_term
|
|
(rename_subst_fo_term bnd1 identity identity)
|
|
((rename_subst_symbol s0 identity))
|
|
((rename_subst_fo_term s1 identity identity))
|
|
=
|
|
(rename_subst_fo_term (subst_compose_fo_term bnd1 s0 s1)
|
|
identity identity)
|
|
} ;
|
|
()
|
|
end
|
|
|
|
let lemma nlmodel_rename_commutation_lemma_fo_formula
|
|
(t:nl_fo_formula 'b0 'b1) (fr0:'b0 -> (symbol 'c0))
|
|
(bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
|
|
(fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1))
|
|
(s1:'c1 -> 'd1) : unit
|
|
ensures {
|
|
nlmodel_fo_formula t (rename_subst_symbol fr0 s0)
|
|
(rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr1 s0 s1)
|
|
(rename_subst_fo_term bnd1 s0 s1)
|
|
= rename_fo_formula (nlmodel_fo_formula t fr0 bnd0 fr1 bnd1) s0 s1 }
|
|
=
|
|
nlmodel_subst_commutation_lemma_fo_formula t fr0 bnd0
|
|
(subst_of_rename_symbol s0) fr1 bnd1 (subst_of_rename_fo_term s1)
|
|
|
|
predicate correct_indexes_fo_formula (t:nl_fo_formula 'b0 'b1) =
|
|
match t with | NL_Forall v0 -> correct_indexes_fo_formula v0
|
|
| NL_Exists v0 -> correct_indexes_fo_formula v0
|
|
| NL_And v0 v1 ->
|
|
correct_indexes_fo_formula v0 /\ correct_indexes_fo_formula v1
|
|
| NL_Or v0 v1 ->
|
|
correct_indexes_fo_formula v0 /\ correct_indexes_fo_formula v1
|
|
| NL_Not v0 -> correct_indexes_fo_formula v0 | NL_FTrue -> true
|
|
| NL_FFalse -> true
|
|
| NL_PApp v0 v1 ->
|
|
correct_indexes_symbol v0 /\ correct_indexes_fo_term_list v1
|
|
end
|
|
|
|
function bound_depth_of_symbol_in_fo_formula (t:nl_fo_formula 'b0 'b1) :
|
|
int =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
let b = bound_depth_of_symbol_in_fo_formula v0 in let a = b in a
|
|
| NL_Exists v0 ->
|
|
let b = bound_depth_of_symbol_in_fo_formula v0 in let a = b in a
|
|
| NL_And v0 v1 ->
|
|
let b = bound_depth_of_symbol_in_fo_formula v0 in let a = b in
|
|
let b = bound_depth_of_symbol_in_fo_formula v1 in
|
|
let a = if a > b then a else b in a
|
|
| NL_Or v0 v1 ->
|
|
let b = bound_depth_of_symbol_in_fo_formula v0 in let a = b in
|
|
let b = bound_depth_of_symbol_in_fo_formula v1 in
|
|
let a = if a > b then a else b in a
|
|
| NL_Not v0 ->
|
|
let b = bound_depth_of_symbol_in_fo_formula v0 in let a = b in a
|
|
| NL_FTrue -> 0 | NL_FFalse -> 0
|
|
| NL_PApp v0 v1 ->
|
|
let b = bound_depth_of_symbol_in_symbol v0 in let a = b in
|
|
let b = bound_depth_of_symbol_in_fo_term_list v1 in
|
|
let a = if a > b then a else b in a
|
|
end
|
|
|
|
with bound_depth_of_fo_term_in_fo_formula (t:nl_fo_formula 'b0 'b1) : int =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
let b = bound_depth_of_fo_term_in_fo_formula v0 in
|
|
let b = if b < 1 then 0 else b - 1 in let a = b in a
|
|
| NL_Exists v0 ->
|
|
let b = bound_depth_of_fo_term_in_fo_formula v0 in
|
|
let b = if b < 1 then 0 else b - 1 in let a = b in a
|
|
| NL_And v0 v1 ->
|
|
let b = bound_depth_of_fo_term_in_fo_formula v0 in let a = b in
|
|
let b = bound_depth_of_fo_term_in_fo_formula v1 in
|
|
let a = if a > b then a else b in a
|
|
| NL_Or v0 v1 ->
|
|
let b = bound_depth_of_fo_term_in_fo_formula v0 in let a = b in
|
|
let b = bound_depth_of_fo_term_in_fo_formula v1 in
|
|
let a = if a > b then a else b in a
|
|
| NL_Not v0 ->
|
|
let b = bound_depth_of_fo_term_in_fo_formula v0 in let a = b in a
|
|
| NL_FTrue -> 0 | NL_FFalse -> 0
|
|
| NL_PApp v0 v1 ->
|
|
let b = bound_depth_of_fo_term_in_fo_term_list v1 in let a = b in a
|
|
end
|
|
|
|
let rec lemma bound_depth_of_symbol_in_fo_formula_nonnegative
|
|
(t:nl_fo_formula 'b0 'b1) : unit
|
|
requires { correct_indexes_fo_formula t }
|
|
ensures { bound_depth_of_symbol_in_fo_formula t >= 0 }
|
|
variant { nlsize_fo_formula t } =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_Exists v0 ->
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_And v0 v1 ->
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v0 ;
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v1 ; ()
|
|
| NL_Or v0 v1 ->
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v0 ;
|
|
bound_depth_of_symbol_in_fo_formula_nonnegative v1 ; ()
|
|
| NL_Not v0 -> bound_depth_of_symbol_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_FTrue -> () | NL_FFalse -> ()
|
|
| NL_PApp v0 v1 ->
|
|
bound_depth_of_symbol_in_symbol_nonnegative v0 ;
|
|
bound_depth_of_symbol_in_fo_term_list_nonnegative v1 ; ()
|
|
end
|
|
|
|
with lemma bound_depth_of_fo_term_in_fo_formula_nonnegative
|
|
(t:nl_fo_formula 'b0 'b1) : unit
|
|
requires { correct_indexes_fo_formula t }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula t >= 0 }
|
|
variant { nlsize_fo_formula t } =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_Exists v0 ->
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_And v0 v1 ->
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ;
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v1 ; ()
|
|
| NL_Or v0 v1 ->
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ;
|
|
bound_depth_of_fo_term_in_fo_formula_nonnegative v1 ; ()
|
|
| NL_Not v0 -> bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ; ()
|
|
| NL_FTrue -> () | NL_FFalse -> ()
|
|
| NL_PApp v0 v1 ->
|
|
() ; bound_depth_of_fo_term_in_fo_term_list_nonnegative v1 ; ()
|
|
end
|
|
|
|
let rec lemma model_equal_fo_formula (t:nl_fo_formula 'b0 'b1)
|
|
(fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
|
|
(bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
|
|
(fr11: 'b1 -> (fo_term 'c0 'c1)) (fr21: 'b1 -> (fo_term 'c0 'c1))
|
|
(bnd11: int -> (fo_term 'c0 'c1)) (bnd21: int -> (fo_term 'c0 'c1)) :
|
|
unit
|
|
requires {
|
|
forall i:int. 0 <= i < bound_depth_of_symbol_in_fo_formula t ->
|
|
bnd10 i = bnd20 i
|
|
}
|
|
requires { fr10 = fr20 }
|
|
requires {
|
|
forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_formula t ->
|
|
bnd11 i = bnd21 i
|
|
}
|
|
requires { fr11 = fr21 } requires { correct_indexes_fo_formula t }
|
|
ensures { nlmodel_fo_formula t fr10 bnd10 fr11 bnd11 =
|
|
nlmodel_fo_formula t fr20 bnd20 fr21 bnd21 }
|
|
variant { nlsize_fo_formula t } =
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
model_equal_fo_formula v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity (compose some identity)))
|
|
((rename_subst_fo_term fr21 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity identity))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd21) identity identity)) ;
|
|
()
|
|
| NL_Exists v0 ->
|
|
model_equal_fo_formula v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity (compose some identity)))
|
|
((rename_subst_fo_term fr21 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity identity))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd21) identity identity)) ;
|
|
()
|
|
| NL_And v0 v1 ->
|
|
model_equal_fo_formula v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
model_equal_fo_formula v1 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
()
|
|
| NL_Or v0 v1 ->
|
|
model_equal_fo_formula v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
model_equal_fo_formula v1 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
()
|
|
| NL_Not v0 ->
|
|
model_equal_fo_formula v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ; ()
|
|
| NL_FTrue -> () | NL_FFalse -> ()
|
|
| NL_PApp v0 v1 ->
|
|
model_equal_symbol v0 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity)) ;
|
|
model_equal_fo_term_list v1 ((rename_subst_symbol fr10 identity))
|
|
((rename_subst_symbol fr20 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr11 identity identity))
|
|
((rename_subst_fo_term fr21 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)) ;
|
|
()
|
|
end
|
|
|
|
predicate nlimpl_fo_formula_ok (t:nlimpl_fo_formula) =
|
|
nlmodel_fo_formula t.nlrepr_fo_formula_field subst_id_symbol
|
|
(const (Var_symbol ((-1)))) subst_id_fo_term
|
|
(const (Var_fo_term ((-1)))) = t.model_fo_formula_field
|
|
/\ correct_indexes_fo_formula t.nlrepr_fo_formula_field /\
|
|
bound_depth_of_symbol_in_fo_formula t.nlrepr_fo_formula_field = 0 /\
|
|
bound_depth_of_fo_term_in_fo_formula t.nlrepr_fo_formula_field = 0 /\
|
|
(forall x:int.
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field -> (x) <
|
|
(t.nlfree_var_symbol_set_abstraction_fo_formula_field))
|
|
/\
|
|
(forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field -> (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_fo_formula_field))
|
|
|
|
predicate cons_ok_fo_formula (c:cons_fo_formula) =
|
|
match c with | NLC_Forall v0 v1 -> nlimpl_fo_formula_ok v1
|
|
| NLC_Exists v0 v1 -> nlimpl_fo_formula_ok v1
|
|
| NLC_And v0 v1 -> nlimpl_fo_formula_ok v0 /\ nlimpl_fo_formula_ok v1
|
|
| NLC_Or v0 v1 -> nlimpl_fo_formula_ok v0 /\ nlimpl_fo_formula_ok v1
|
|
| NLC_Not v0 -> nlimpl_fo_formula_ok v0 | NLC_FTrue -> true
|
|
| NLC_FFalse -> true
|
|
| NLC_PApp v0 v1 -> nlimpl_symbol_ok v0 /\ nlimpl_fo_term_list_ok v1
|
|
end
|
|
|
|
predicate cons_rel_fo_formula (c:cons_fo_formula) (t:nlimpl_fo_formula) =
|
|
match c with
|
|
| NLC_Forall v0 v1 -> t.model_fo_formula_field =
|
|
Forall
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
| NLC_Exists v0 v1 -> t.model_fo_formula_field =
|
|
Exists
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
| NLC_And v0 v1 -> t.model_fo_formula_field =
|
|
And (rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
| NLC_Or v0 v1 -> t.model_fo_formula_field =
|
|
Or (rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
| NLC_Not v0 -> t.model_fo_formula_field =
|
|
Not (rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
| NLC_FTrue -> t.model_fo_formula_field = FTrue
|
|
| NLC_FFalse -> t.model_fo_formula_field = FFalse
|
|
| NLC_PApp v0 v1 -> t.model_fo_formula_field =
|
|
PApp (rename_symbol v0.model_symbol_field identity)
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity identity)
|
|
end
|
|
|
|
predicate cons_open_rel_fo_formula (c:cons_fo_formula)
|
|
(t:nlimpl_fo_formula) =
|
|
match c with
|
|
| NLC_Forall v0 v1 ->
|
|
match t.model_fo_formula_field with
|
|
| Forall w0 ->
|
|
v1.model_fo_formula_field =
|
|
(rename_fo_formula w0 identity (ocase identity v0))
|
|
| Exists w0 -> false | And w0 w1 -> false | Or w0 w1 -> false
|
|
| Not w0 -> false | FTrue -> false | FFalse -> false
|
|
| PApp w0 w1 -> false
|
|
end
|
|
| NLC_Exists v0 v1 ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 ->
|
|
v1.model_fo_formula_field =
|
|
(rename_fo_formula w0 identity (ocase identity v0))
|
|
| And w0 w1 -> false | Or w0 w1 -> false | Not w0 -> false
|
|
| FTrue -> false | FFalse -> false | PApp w0 w1 -> false
|
|
end
|
|
| NLC_And v0 v1 ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false
|
|
| And w0 w1 ->
|
|
v0.model_fo_formula_field =
|
|
(rename_fo_formula w0 identity identity) /\
|
|
v1.model_fo_formula_field =
|
|
(rename_fo_formula w1 identity identity)
|
|
| Or w0 w1 -> false | Not w0 -> false | FTrue -> false
|
|
| FFalse -> false | PApp w0 w1 -> false
|
|
end
|
|
| NLC_Or v0 v1 ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false | And w0 w1 -> false
|
|
| Or w0 w1 ->
|
|
v0.model_fo_formula_field =
|
|
(rename_fo_formula w0 identity identity) /\
|
|
v1.model_fo_formula_field =
|
|
(rename_fo_formula w1 identity identity)
|
|
| Not w0 -> false | FTrue -> false | FFalse -> false
|
|
| PApp w0 w1 -> false
|
|
end
|
|
| NLC_Not v0 ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false | And w0 w1 -> false | Or w0 w1 -> false
|
|
| Not w0 ->
|
|
v0.model_fo_formula_field =
|
|
(rename_fo_formula w0 identity identity)
|
|
| FTrue -> false | FFalse -> false | PApp w0 w1 -> false
|
|
end
|
|
| NLC_FTrue ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false | And w0 w1 -> false | Or w0 w1 -> false
|
|
| Not w0 -> false | FTrue -> true | FFalse -> false
|
|
| PApp w0 w1 -> false
|
|
end
|
|
| NLC_FFalse ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false | And w0 w1 -> false | Or w0 w1 -> false
|
|
| Not w0 -> false | FTrue -> false | FFalse -> true
|
|
| PApp w0 w1 -> false
|
|
end
|
|
| NLC_PApp v0 v1 ->
|
|
match t.model_fo_formula_field with | Forall w0 -> false
|
|
| Exists w0 -> false | And w0 w1 -> false | Or w0 w1 -> false
|
|
| Not w0 -> false | FTrue -> false | FFalse -> false
|
|
| PApp w0 w1 ->
|
|
v0.model_symbol_field = (rename_symbol w0 identity) /\
|
|
v1.model_fo_term_list_field =
|
|
(rename_fo_term_list w1 identity identity)
|
|
end
|
|
end
|
|
|
|
|
|
end
|
|
|
|
module Impl
|
|
use option.Option
|
|
use int.Int
|
|
use Nat.Nat
|
|
use Functions.Func
|
|
use OptionFuncs.Funcs
|
|
use Sum.Sum
|
|
use Firstorder_symbol_spec.Spec
|
|
use Firstorder_symbol_impl.Types
|
|
use Firstorder_symbol_impl.Logic
|
|
use Firstorder_symbol_impl.Impl
|
|
use Firstorder_term_spec.Spec
|
|
use Firstorder_term_impl.Types
|
|
use Firstorder_term_impl.Logic
|
|
use Firstorder_term_impl.Impl
|
|
use Firstorder_formula_spec.Spec
|
|
use Types
|
|
use Logic
|
|
let rec bind_var_symbol_in_fo_formula (t:nl_fo_formula int int) (x:int)
|
|
(i:int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd0: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd1: int -> (fo_term 'b0 'b1)) : nl_fo_formula int int
|
|
requires { correct_indexes_fo_formula t }
|
|
requires { bound_depth_of_symbol_in_fo_formula t <= i }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { bound_depth_of_symbol_in_fo_formula result <= i + 1 }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula t =
|
|
bound_depth_of_fo_term_in_fo_formula result }
|
|
ensures { nlmodel_fo_formula result fr0 bnd0 fr1 bnd1 =
|
|
nlmodel_fo_formula t (update fr0 x (bnd0 i)) bnd0 fr1 bnd1 }
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_Forall
|
|
(bind_var_symbol_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity)))
|
|
| NL_Exists v0 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_Exists
|
|
(bind_var_symbol_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity)))
|
|
| NL_And v0 v1 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_And
|
|
(bind_var_symbol_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_symbol_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_Or
|
|
(bind_var_symbol_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_symbol_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Not v0 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_Not
|
|
(bind_var_symbol_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
assert { (rename_symbol (bnd0 i) identity) =
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol (update fr0 x (bnd0 i)) identity))
|
|
((update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (bnd0 i) identity)))
|
|
};
|
|
assert { (rename_subst_symbol (update fr0 x (bnd0 i)) identity) =
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(eval ((rename_subst_symbol bnd0 identity)) (i+0)))
|
|
};
|
|
NL_PApp
|
|
(bind_var_symbol_in_symbol v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity)))
|
|
(bind_var_symbol_in_fo_term_list v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
with bind_var_fo_term_in_fo_formula (t:nl_fo_formula int int) (x:int)
|
|
(i:int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd0: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd1: int -> (fo_term 'b0 'b1)) : nl_fo_formula int int
|
|
requires { correct_indexes_fo_formula t }
|
|
requires { bound_depth_of_fo_term_in_fo_formula t <= i }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula result <= i + 1 }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_symbol_in_fo_formula t =
|
|
bound_depth_of_symbol_in_fo_formula result }
|
|
ensures { nlmodel_fo_formula result fr0 bnd0 fr1 bnd1 =
|
|
nlmodel_fo_formula t fr0 bnd0 (update fr1 x (bnd1 i)) bnd1 }
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert { (rename_fo_term (bnd1 i) identity (compose some identity)) =
|
|
(eval
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity))
|
|
(i+1))
|
|
};
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
(compose some identity)))
|
|
((update
|
|
((rename_subst_fo_term fr1 identity
|
|
(compose some identity)))
|
|
x
|
|
(rename_fo_term (bnd1 i) identity (compose some identity))))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
(compose some identity))
|
|
=
|
|
(update
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
x
|
|
(eval
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity))
|
|
(i+1)))
|
|
};
|
|
NL_Forall
|
|
(bind_var_fo_term_in_fo_formula v0 x (i+1)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity)))
|
|
| NL_Exists v0 ->
|
|
assert { (rename_fo_term (bnd1 i) identity (compose some identity)) =
|
|
(eval
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity identity))
|
|
(i+1))
|
|
};
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
(compose some identity)))
|
|
((update
|
|
((rename_subst_fo_term fr1 identity
|
|
(compose some identity)))
|
|
x
|
|
(rename_fo_term (bnd1 i) identity (compose some identity))))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
(compose some identity))
|
|
=
|
|
(update
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
x
|
|
(eval
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity))
|
|
(i+1)))
|
|
};
|
|
NL_Exists
|
|
(bind_var_fo_term_in_fo_formula v0 x (i+1)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd1) identity
|
|
identity)))
|
|
| NL_And v0 v1 ->
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
NL_And
|
|
(bind_var_fo_term_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_fo_term_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
NL_Or
|
|
(bind_var_fo_term_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
(bind_var_fo_term_in_fo_formula v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_Not v0 ->
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
NL_Not
|
|
(bind_var_fo_term_in_fo_formula v0 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert { (rename_fo_term (bnd1 i) identity identity) =
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)) };
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term (update fr1 x (bnd1 i)) identity
|
|
identity))
|
|
((update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (bnd1 i) identity identity)))
|
|
};
|
|
assert {
|
|
(rename_subst_fo_term (update fr1 x (bnd1 i)) identity identity)
|
|
=
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(eval ((rename_subst_fo_term bnd1 identity identity)) (i+0)))
|
|
};
|
|
NL_PApp (v0)
|
|
(bind_var_fo_term_in_fo_term_list v1 x (i+0)
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd0 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd1 identity identity)))
|
|
end
|
|
|
|
let rec unbind_var_symbol_in_fo_formula (t:nl_fo_formula int int) (i:int)
|
|
(x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_formula int int
|
|
requires { i >= 0 } requires { correct_indexes_fo_formula t }
|
|
requires { bound_depth_of_symbol_in_fo_formula t <= i + 1 }
|
|
requires { correct_indexes_symbol x }
|
|
requires { bound_depth_of_symbol_in_symbol x = 0 }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_symbol_in_fo_formula result <= i }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula result =
|
|
bound_depth_of_fo_term_in_fo_formula t }
|
|
ensures { nlmodel_fo_formula result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_fo_formula t fr0 (update bnd10 i (nlmodel_symbol x fr0 bnd20))
|
|
fr1 bnd11
|
|
}
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Forall
|
|
(unbind_var_symbol_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Exists v0 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Exists
|
|
(unbind_var_symbol_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_And v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_And
|
|
(unbind_var_symbol_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(unbind_var_symbol_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Or
|
|
(unbind_var_symbol_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(unbind_var_symbol_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Not v0 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Not
|
|
(unbind_var_symbol_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol x fr0 bnd20) identity =
|
|
nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(rename_symbol (nlmodel_symbol x fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol
|
|
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) identity)
|
|
=
|
|
update ((rename_subst_symbol bnd10 identity)) (i+0)
|
|
(nlmodel_symbol x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_PApp
|
|
(unbind_var_symbol_in_symbol v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(unbind_var_symbol_in_fo_term_list v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
end
|
|
|
|
with unbind_var_fo_term_in_fo_formula (t:nl_fo_formula int int) (i:int)
|
|
(x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0))
|
|
(ghost bnd21: int -> (fo_term 'b0 'b1)) : nl_fo_formula int int
|
|
requires { i >= 0 } requires { correct_indexes_fo_formula t }
|
|
requires { bound_depth_of_fo_term_in_fo_formula t <= i + 1 }
|
|
requires { correct_indexes_fo_term x }
|
|
requires { bound_depth_of_symbol_in_fo_term x = 0 }
|
|
requires { bound_depth_of_fo_term_in_fo_term x = 0 }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula result <= i }
|
|
ensures { bound_depth_of_symbol_in_fo_formula result =
|
|
bound_depth_of_symbol_in_fo_formula t }
|
|
ensures { nlmodel_fo_formula result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_fo_formula t fr0 bnd10 fr1
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
}
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
(compose some identity)
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)))
|
|
identity identity))
|
|
(update
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
(i+1)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)))
|
|
identity identity)
|
|
=
|
|
update
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
(i+1)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity
|
|
(compose some identity))))
|
|
} ;
|
|
NL_Forall
|
|
(unbind_var_fo_term_in_fo_formula v0 (i+1) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity))))
|
|
| NL_Exists v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
(compose some identity)
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)))
|
|
identity identity))
|
|
(update
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
(i+1)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)))
|
|
identity identity)
|
|
=
|
|
update
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
(i+1)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity
|
|
(compose some identity))))
|
|
} ;
|
|
NL_Exists
|
|
(unbind_var_fo_term_in_fo_formula v0 (i+1) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity))))
|
|
| NL_And v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_And
|
|
(unbind_var_fo_term_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(unbind_var_fo_term_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Or
|
|
(unbind_var_fo_term_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(unbind_var_fo_term_in_fo_formula v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_Not v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Not
|
|
(unbind_var_fo_term_in_fo_formula v0 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
|
|
identity identity)
|
|
=
|
|
update ((rename_subst_fo_term bnd11 identity identity)) (i+0)
|
|
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_PApp (v0)
|
|
(unbind_var_fo_term_in_fo_term_list v1 (i+0) x
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
end
|
|
|
|
let rec subst_base_symbol_in_fo_formula (t:nl_fo_formula int int) (x:int)
|
|
(u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_formula int int
|
|
requires { correct_indexes_fo_formula t }
|
|
requires { correct_indexes_symbol u }
|
|
requires { bound_depth_of_symbol_in_symbol u = 0 }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_symbol_in_fo_formula result =
|
|
bound_depth_of_symbol_in_fo_formula t }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula result =
|
|
bound_depth_of_fo_term_in_fo_formula t }
|
|
ensures { nlmodel_fo_formula result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_fo_formula t (update fr0 x (nlmodel_symbol u fr0 bnd20)) bnd10
|
|
fr1 bnd11
|
|
}
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Forall
|
|
(subst_base_symbol_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Exists v0 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Exists
|
|
(subst_base_symbol_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_And v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_And
|
|
(subst_base_symbol_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(subst_base_symbol_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Or
|
|
(subst_base_symbol_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(subst_base_symbol_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_Not v0 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_Not
|
|
(subst_base_symbol_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
assert { rename_symbol (nlmodel_symbol u fr0 bnd20) identity =
|
|
nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_symbol
|
|
(update fr0 x (nlmodel_symbol u fr0 bnd20)) identity))
|
|
(update ((rename_subst_symbol fr0 identity)) x
|
|
(rename_symbol (nlmodel_symbol u fr0 bnd20) identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_symbol (update fr0 x (nlmodel_symbol u fr0 bnd20))
|
|
identity)
|
|
=
|
|
update ((rename_subst_symbol fr0 identity)) x
|
|
(nlmodel_symbol u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
} ;
|
|
NL_PApp
|
|
(subst_base_symbol_in_symbol v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
(subst_base_symbol_in_fo_term_list v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity)))
|
|
end
|
|
|
|
with subst_base_fo_term_in_fo_formula (t:nl_fo_formula int int) (x:int)
|
|
(u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
|
|
(ghost bnd10: int -> (symbol 'b0)) (ghost fr1: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd11: int -> (fo_term 'b0 'b1))
|
|
(ghost bnd20: int -> (symbol 'b0))
|
|
(ghost bnd21: int -> (fo_term 'b0 'b1)) : nl_fo_formula int int
|
|
requires { correct_indexes_fo_formula t }
|
|
requires { correct_indexes_fo_term u }
|
|
requires { bound_depth_of_symbol_in_fo_term u = 0 }
|
|
requires { bound_depth_of_fo_term_in_fo_term u = 0 }
|
|
variant { nlsize_fo_formula t }
|
|
ensures { correct_indexes_fo_formula result }
|
|
ensures { bound_depth_of_symbol_in_fo_formula result =
|
|
bound_depth_of_symbol_in_fo_formula t }
|
|
ensures { bound_depth_of_fo_term_in_fo_formula result =
|
|
bound_depth_of_fo_term_in_fo_formula t }
|
|
ensures { nlmodel_fo_formula result fr0 bnd10 fr1 bnd11 =
|
|
nlmodel_fo_formula t fr0 bnd10
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) bnd11
|
|
}
|
|
=
|
|
match t with
|
|
| NL_Forall v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
(compose some identity)
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity (compose some identity)))
|
|
(update
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
(compose some identity))
|
|
=
|
|
update
|
|
((rename_subst_fo_term fr1 identity (compose some identity))) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity
|
|
(compose some identity))))
|
|
} ;
|
|
NL_Forall
|
|
(subst_base_fo_term_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity))))
|
|
| NL_Exists v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
(compose some identity)
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity (compose some identity)))
|
|
(update
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity (compose some identity)))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
(compose some identity))
|
|
=
|
|
update
|
|
((rename_subst_fo_term fr1 identity (compose some identity))) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term bnd21 identity
|
|
(compose some identity))))
|
|
} ;
|
|
NL_Exists
|
|
(subst_base_fo_term_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity (compose some identity)))
|
|
((rename_subst_fo_term (shiftb_fo_term bnd11) identity
|
|
identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity (compose some identity))))
|
|
| NL_And v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_And
|
|
(subst_base_fo_term_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(subst_base_fo_term_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_Or v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Or
|
|
(subst_base_fo_term_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
(subst_base_fo_term_in_fo_formula v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_Not v0 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_Not
|
|
(subst_base_fo_term_in_fo_formula v0 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
| NL_FTrue -> NL_FTrue | NL_FFalse -> NL_FFalse
|
|
| NL_PApp v0 v1 ->
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
assert {
|
|
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21) identity
|
|
identity
|
|
=
|
|
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity))
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
((rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21))
|
|
identity identity))
|
|
(update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)
|
|
identity identity))
|
|
} ;
|
|
assert {
|
|
(rename_subst_fo_term
|
|
(update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) identity
|
|
identity)
|
|
=
|
|
update ((rename_subst_fo_term fr1 identity identity)) x
|
|
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
} ;
|
|
NL_PApp (v0)
|
|
(subst_base_fo_term_in_fo_term_list v1 x u
|
|
((rename_subst_symbol fr0 identity))
|
|
((rename_subst_symbol bnd10 identity))
|
|
((rename_subst_fo_term fr1 identity identity))
|
|
((rename_subst_fo_term bnd11 identity identity))
|
|
((rename_subst_symbol bnd20 identity))
|
|
((rename_subst_fo_term bnd21 identity identity)))
|
|
end
|
|
|
|
let construct_fo_formula (c:cons_fo_formula) : nlimpl_fo_formula
|
|
requires { cons_ok_fo_formula c } ensures { nlimpl_fo_formula_ok result }
|
|
ensures { cons_rel_fo_formula c result }
|
|
(*ensures { cons_open_rel_fo_formula c result }*) =
|
|
match c with
|
|
| NLC_Forall v0 v1 -> assert { nlimpl_fo_formula_ok v1 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_Forall
|
|
(let v1 = v1.nlrepr_fo_formula_field in
|
|
let v1 =
|
|
bind_var_fo_term_in_fo_formula v1 v0 0
|
|
(ghost
|
|
(rename_subst_symbol
|
|
(subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
(ghost
|
|
(rename_subst_symbol (const (Var_symbol (-1)))
|
|
identity))
|
|
(ghost
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int)))
|
|
identity (compose some identity)))
|
|
(ghost
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term (const (Var_fo_term (-1))))
|
|
identity identity))
|
|
in v1)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
v1.nlfree_var_symbol_set_abstraction_fo_formula_field ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
v1.nlfree_var_fo_term_set_abstraction_fo_formula_field ;
|
|
model_fo_formula_field = ghost
|
|
(Forall
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula (Some x)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\
|
|
eval ((update (compose some identity) v0 None)) y = (Some x))
|
|
-> y <> v0 && (Some x) = eval ((compose some identity)) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None)))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_formula (Some x)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None)))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
((update
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
(compose some identity))
|
|
v0 (Var_fo_term None)))
|
|
} ;
|
|
assert {
|
|
rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None)
|
|
=
|
|
(update
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
(compose some identity))
|
|
v0 (Var_fo_term None))
|
|
} ;
|
|
model_equal_fo_formula v1.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
((rename_subst_fo_term (shiftb_fo_term (const (Var_fo_term (-1))))
|
|
identity identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
(update (compose some identity) v0 None)) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual
|
|
(rcompose ((update (compose some identity) v0 None))
|
|
((ocase identity v0)))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert {
|
|
rcompose ((update (compose some identity) v0 None))
|
|
((ocase identity v0))
|
|
= (identity : (int) -> (int)) } ;*)
|
|
res
|
|
| NLC_Exists v0 v1 -> assert { nlimpl_fo_formula_ok v1 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_Exists
|
|
(let v1 = v1.nlrepr_fo_formula_field in
|
|
let v1 =
|
|
bind_var_fo_term_in_fo_formula v1 v0 0
|
|
(ghost
|
|
(rename_subst_symbol
|
|
(subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
(ghost
|
|
(rename_subst_symbol (const (Var_symbol (-1)))
|
|
identity))
|
|
(ghost
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int)))
|
|
identity (compose some identity)))
|
|
(ghost
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term (const (Var_fo_term (-1))))
|
|
identity identity))
|
|
in v1)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
v1.nlfree_var_symbol_set_abstraction_fo_formula_field ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
v1.nlfree_var_fo_term_set_abstraction_fo_formula_field ;
|
|
model_fo_formula_field = ghost
|
|
(Exists
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula (Some x)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None))
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\
|
|
eval ((update (compose some identity) v0 None)) y = (Some x))
|
|
-> y <> v0 && (Some x) = eval ((compose some identity)) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None)))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_formula (Some x)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
(update (compose some identity) v0 None)))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
((update
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
(compose some identity))
|
|
v0 (Var_fo_term None)))
|
|
} ;
|
|
assert {
|
|
rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None)
|
|
=
|
|
(update
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
(compose some identity))
|
|
v0 (Var_fo_term None))
|
|
} ;
|
|
model_equal_fo_formula v1.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(update (compose some identity) v0 None))
|
|
((rename_subst_fo_term (shiftb_fo_term (const (Var_fo_term (-1))))
|
|
identity identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
(update (compose some identity) v0 None)) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual
|
|
(rcompose ((update (compose some identity) v0 None))
|
|
((ocase identity v0)))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert {
|
|
rcompose ((update (compose some identity) v0 None))
|
|
((ocase identity v0))
|
|
= (identity : (int) -> (int)) } ;*)
|
|
res
|
|
| NLC_And v0 v1 -> assert { nlimpl_fo_formula_ok v0 } ;
|
|
assert { nlimpl_fo_formula_ok v1 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_And (let v0 = v0.nlrepr_fo_formula_field in v0)
|
|
(let v1 = v1.nlrepr_fo_formula_field in v1)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
(v1.nlfree_var_symbol_set_abstraction_fo_formula_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
(v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)) ;
|
|
model_fo_formula_field = ghost
|
|
(And
|
|
(rename_fo_formula v0.model_fo_formula_field identity
|
|
identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity)) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
\/
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
\/
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v0.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v1.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
res
|
|
| NLC_Or v0 v1 -> assert { nlimpl_fo_formula_ok v0 } ;
|
|
assert { nlimpl_fo_formula_ok v1 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_Or (let v0 = v0.nlrepr_fo_formula_field in v0)
|
|
(let v1 = v1.nlrepr_fo_formula_field in v1)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
(v1.nlfree_var_symbol_set_abstraction_fo_formula_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
(v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)) ;
|
|
model_fo_formula_field = ghost
|
|
(Or
|
|
(rename_fo_formula v0.model_fo_formula_field identity
|
|
identity)
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity)) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v1.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v1.model_fo_formula_field
|
|
&& (x) < (v1.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
\/
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
\/
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v1.model_fo_formula_field identity
|
|
identity))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v0.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v1.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
res
|
|
| NLC_Not v0 -> assert { nlimpl_fo_formula_ok v0 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_Not (let v0 = v0.nlrepr_fo_formula_field in v0)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
v0.nlfree_var_symbol_set_abstraction_fo_formula_field ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
v0.nlfree_var_fo_term_set_abstraction_fo_formula_field ;
|
|
model_fo_formula_field = ghost
|
|
(Not
|
|
(rename_fo_formula v0.model_fo_formula_field identity
|
|
identity)) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_symbol_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y v0.model_fo_formula_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field)
|
|
&& is_fo_term_free_var_in_fo_formula x v0.model_fo_formula_field
|
|
&& (x) < (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_formula x
|
|
(rename_fo_formula v0.model_fo_formula_field identity identity))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_formula v0.nlrepr_fo_formula_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
res
|
|
| NLC_FTrue ->
|
|
let res =
|
|
{ nlrepr_fo_formula_field = (NL_FTrue) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = 0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = 0 ;
|
|
model_fo_formula_field = ghost (FTrue) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
res
|
|
| NLC_FFalse ->
|
|
let res =
|
|
{ nlrepr_fo_formula_field = (NL_FFalse) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = 0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = 0 ;
|
|
model_fo_formula_field = ghost (FFalse) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(false) && (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
res
|
|
| NLC_PApp v0 v1 -> assert { nlimpl_symbol_ok v0 } ;
|
|
assert { nlimpl_fo_term_list_ok v1 } ;
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
(NL_PApp (let v0 = v0.nlrepr_symbol_field in v0)
|
|
(let v1 = v1.nlrepr_fo_term_list_field in v1)) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in
|
|
aux (v0.nlfree_var_symbol_set_abstraction_symbol_field)
|
|
(v1.nlfree_var_symbol_set_abstraction_fo_term_list_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field ;
|
|
model_fo_formula_field = ghost
|
|
(PApp (rename_symbol v0.model_symbol_field identity)
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity
|
|
identity)) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_symbol x
|
|
(rename_symbol v0.model_symbol_field identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_symbol y v0.model_symbol_field /\
|
|
eval (identity) y = x) -> x = eval (identity) y && x = y &&
|
|
is_symbol_free_var_in_symbol x v0.model_symbol_field)
|
|
&& is_symbol_free_var_in_symbol x v0.model_symbol_field && (x) <
|
|
(v0.nlfree_var_symbol_set_abstraction_symbol_field) && (x) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_term_list x
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity
|
|
identity)
|
|
->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_term_list y
|
|
v1.model_fo_term_list_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_symbol_free_var_in_fo_term_list x
|
|
v1.model_fo_term_list_field)
|
|
&&
|
|
is_symbol_free_var_in_fo_term_list x v1.model_fo_term_list_field
|
|
&& (x) <
|
|
(v1.nlfree_var_symbol_set_abstraction_fo_term_list_field) && (x)
|
|
< (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_term_list x
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity
|
|
identity)
|
|
->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_term_list y
|
|
v1.model_fo_term_list_field
|
|
/\ eval (identity) y = x) -> x = eval (identity) y &&
|
|
x = y &&
|
|
is_fo_term_free_var_in_fo_term_list x
|
|
v1.model_fo_term_list_field)
|
|
&&
|
|
is_fo_term_free_var_in_fo_term_list x v1.model_fo_term_list_field
|
|
&& (x) <
|
|
(v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field) && (x)
|
|
< (res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_symbol_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_symbol_free_var_in_symbol x
|
|
(rename_symbol v0.model_symbol_field identity) \/
|
|
is_symbol_free_var_in_fo_term_list x
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity
|
|
identity))
|
|
&& (x) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x:int.
|
|
is_fo_term_free_var_in_fo_formula x res.model_fo_formula_field ->
|
|
(is_fo_term_free_var_in_fo_term_list x
|
|
(rename_fo_term_list v1.model_fo_term_list_field identity
|
|
identity))
|
|
&& (x) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
model_equal_symbol v0.nlrepr_symbol_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
assert {
|
|
extensionalEqual (rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_symbol subst_id_symbol identity =
|
|
(rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
|
|
identity)
|
|
} ;
|
|
assert {
|
|
extensionalEqual
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity))
|
|
} ;
|
|
assert { rename_subst_fo_term subst_id_fo_term identity identity =
|
|
(rename_subst_fo_term
|
|
(subst_id_fo_term:(int)->(fo_term (int) (int))) identity
|
|
identity)
|
|
} ;
|
|
model_equal_fo_term_list v1.nlrepr_fo_term_list_field
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
((rename_subst_symbol (const (Var_symbol (-1))) identity))
|
|
(rename_subst_symbol (const (Var_symbol (-1))) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
((rename_subst_fo_term (const (Var_fo_term (-1))) identity
|
|
identity))
|
|
(rename_subst_fo_term (const (Var_fo_term (-1))) identity identity) ;
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
(*assert {
|
|
extensionalEqual (rcompose (identity) (identity))
|
|
((identity : (int) -> (int)))
|
|
} ;
|
|
assert { rcompose (identity) (identity) = (identity : (int) -> (int))
|
|
} ;*)
|
|
res
|
|
end
|
|
|
|
let destruct_fo_formula (t:nlimpl_fo_formula) : cons_fo_formula
|
|
requires { nlimpl_fo_formula_ok t } ensures { cons_ok_fo_formula result }
|
|
ensures { cons_rel_fo_formula result t }
|
|
ensures { cons_open_rel_fo_formula result t } =
|
|
let fv0 = t.nlfree_var_symbol_set_abstraction_fo_formula_field in
|
|
let fv1 = t.nlfree_var_fo_term_set_abstraction_fo_formula_field in
|
|
match t.nlrepr_fo_formula_field with
|
|
| NL_Forall v0 ->
|
|
let w0 = fv1 in
|
|
let fv1 =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in aux ((1 + (w0))) (fv1))
|
|
in
|
|
assert { t.model_fo_formula_field =
|
|
Forall
|
|
(nlmodel_fo_formula v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity))
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
} ;
|
|
let (mv0) =
|
|
match t.model_fo_formula_field with | Forall x0 -> (x0)
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> absurd
|
|
| FFalse -> absurd | PApp x0 x1 -> absurd
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_fo_formula v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity)))
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v0 <= 1 } ;
|
|
assert {
|
|
forall x:(option int). is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
match x with | None -> true
|
|
| Some x ->
|
|
is_fo_term_free_var_in_fo_formula x
|
|
t.model_fo_formula_field
|
|
&& (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
end
|
|
} ;
|
|
assert {
|
|
eval
|
|
((update (const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
0 (Var_fo_term w0)))
|
|
0
|
|
=
|
|
(rename_fo_term (Var_fo_term None) (identity)
|
|
((ocase identity w0)))
|
|
=
|
|
eval
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
(identity) ((ocase identity w0)))
|
|
0
|
|
} ;
|
|
model_equal_fo_formula v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity)))
|
|
(identity) ((ocase identity w0))) ((update
|
|
(const
|
|
(Var_fo_term (-1)) :
|
|
int
|
|
-> (fo_term int int))
|
|
0 (Var_fo_term w0)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
(identity) ((ocase identity w0))) ;
|
|
let ghost mrv0 = rename_fo_formula mv0 identity (ocase identity w0) in
|
|
let v0 =
|
|
unbind_var_fo_term_in_fo_formula v0 0 (NLFVar_fo_term w0)
|
|
(ghost subst_id_symbol)
|
|
(ghost (const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(ghost subst_id_fo_term)
|
|
(ghost (const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
(ghost (const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(ghost (const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
in
|
|
let resv0 =
|
|
{ nlrepr_fo_formula_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv0 ;
|
|
}
|
|
in let res = NLC_Forall w0 resv0 in
|
|
assert {
|
|
forall x:(option int). is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
match x with
|
|
| None -> eval (identity) (None) =
|
|
eval ((update (compose some identity) w0 None)) w0 =
|
|
eval
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None)))
|
|
(None)
|
|
| Some x -> x <> w0 && eval (identity) ((Some x)) =
|
|
eval ((update (compose some identity) w0 None)) x =
|
|
eval
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None)))
|
|
((Some x))
|
|
end
|
|
} ;
|
|
free_var_equivalence_of_rename_fo_formula mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None))) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv0 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:(option int).
|
|
(is_fo_term_free_var_in_fo_formula y mv0 /\
|
|
eval ((ocase identity w0)) y = x)
|
|
->
|
|
match y with | None -> x = w0 && (x) < (fv1)
|
|
| Some y -> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x
|
|
t.model_fo_formula_field
|
|
&& (x) < (fv1)
|
|
end )
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
| NL_Exists v0 ->
|
|
let w0 = fv1 in
|
|
let fv1 =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } =
|
|
if a < b then b else a in aux ((1 + (w0))) (fv1))
|
|
in
|
|
assert { t.model_fo_formula_field =
|
|
Exists
|
|
(nlmodel_fo_formula v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity))
|
|
(rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
} ;
|
|
let (mv0) =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> (x0) | And x0 x1 -> absurd | Or x0 x1 -> absurd
|
|
| Not x0 -> absurd | FTrue -> absurd | FFalse -> absurd
|
|
| PApp x0 x1 -> absurd
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_fo_formula v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity)))
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v0 <= 1 } ;
|
|
assert {
|
|
forall x:(option int). is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
match x with | None -> true
|
|
| Some x ->
|
|
is_fo_term_free_var_in_fo_formula x
|
|
t.model_fo_formula_field
|
|
&& (x) <
|
|
(t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
end
|
|
} ;
|
|
assert {
|
|
eval
|
|
((update (const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
0 (Var_fo_term w0)))
|
|
0
|
|
=
|
|
(rename_fo_term (Var_fo_term None) (identity)
|
|
((ocase identity w0)))
|
|
=
|
|
eval
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
(identity) ((ocase identity w0)))
|
|
0
|
|
} ;
|
|
model_equal_fo_formula v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity
|
|
(compose some identity)))
|
|
(identity) ((ocase identity w0))) ((update
|
|
(const
|
|
(Var_fo_term (-1)) :
|
|
int
|
|
-> (fo_term int int))
|
|
0 (Var_fo_term w0)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(shiftb_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
identity identity))
|
|
(identity) ((ocase identity w0))) ;
|
|
let ghost mrv0 = rename_fo_formula mv0 identity (ocase identity w0) in
|
|
let v0 =
|
|
unbind_var_fo_term_in_fo_formula v0 0 (NLFVar_fo_term w0)
|
|
(ghost subst_id_symbol)
|
|
(ghost (const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(ghost subst_id_fo_term)
|
|
(ghost (const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
(ghost (const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(ghost (const (Var_fo_term (-1)) : int -> (fo_term int int)))
|
|
in
|
|
let resv0 =
|
|
{ nlrepr_fo_formula_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv0 ;
|
|
}
|
|
in let res = NLC_Exists w0 resv0 in
|
|
assert {
|
|
forall x:(option int). is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
match x with
|
|
| None -> eval (identity) (None) =
|
|
eval ((update (compose some identity) w0 None)) w0 =
|
|
eval
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None)))
|
|
(None)
|
|
| Some x -> x <> w0 && eval (identity) ((Some x)) =
|
|
eval ((update (compose some identity) w0 None)) x =
|
|
eval
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None)))
|
|
((Some x))
|
|
end
|
|
} ;
|
|
free_var_equivalence_of_rename_fo_formula mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose ((ocase identity w0))
|
|
((update (compose some identity) w0 None))) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv0 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:(option int).
|
|
(is_fo_term_free_var_in_fo_formula y mv0 /\
|
|
eval ((ocase identity w0)) y = x)
|
|
->
|
|
match y with | None -> x = w0 && (x) < (fv1)
|
|
| Some y -> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x
|
|
t.model_fo_formula_field
|
|
&& (x) < (fv1)
|
|
end )
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
| NL_And v0 v1 ->
|
|
assert { t.model_fo_formula_field =
|
|
And
|
|
(nlmodel_fo_formula v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(nlmodel_fo_formula v1
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
let (mv0 , mv1) =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> (x0 , x1)
|
|
| Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> absurd
|
|
| FFalse -> absurd | PApp x0 x1 -> absurd
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_fo_formula v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { mv1 =
|
|
nlmodel_fo_formula v1
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv1 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv1 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
model_equal_fo_formula v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
model_equal_fo_formula v1 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
let ghost mrv0 = rename_fo_formula mv0 identity identity in
|
|
let ghost mrv1 = rename_fo_formula mv1 identity identity in
|
|
let resv0 =
|
|
{ nlrepr_fo_formula_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv0 ;
|
|
}
|
|
in
|
|
let resv1 =
|
|
{ nlrepr_fo_formula_field = v1 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv1 ;
|
|
}
|
|
in let res = NLC_And resv0 resv1 in
|
|
free_var_equivalence_of_rename_fo_formula mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
free_var_equivalence_of_rename_fo_formula mv1 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv0 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv0 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv1 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv1 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
| NL_Or v0 v1 ->
|
|
assert { t.model_fo_formula_field =
|
|
Or
|
|
(nlmodel_fo_formula v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(nlmodel_fo_formula v1
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
let (mv0 , mv1) =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> (x0 , x1) | Not x0 -> absurd | FTrue -> absurd
|
|
| FFalse -> absurd | PApp x0 x1 -> absurd
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_fo_formula v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { mv1 =
|
|
nlmodel_fo_formula v1
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv1 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv1 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
model_equal_fo_formula v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
model_equal_fo_formula v1 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
let ghost mrv0 = rename_fo_formula mv0 identity identity in
|
|
let ghost mrv1 = rename_fo_formula mv1 identity identity in
|
|
let resv0 =
|
|
{ nlrepr_fo_formula_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv0 ;
|
|
}
|
|
in
|
|
let resv1 =
|
|
{ nlrepr_fo_formula_field = v1 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv1 ;
|
|
}
|
|
in let res = NLC_Or resv0 resv1 in
|
|
free_var_equivalence_of_rename_fo_formula mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
free_var_equivalence_of_rename_fo_formula mv1 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv0 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv0 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv1 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv1 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv1 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
| NL_Not v0 ->
|
|
assert { t.model_fo_formula_field =
|
|
Not
|
|
(nlmodel_fo_formula v0
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
let (mv0) =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> absurd | Not x0 -> (x0) | FTrue -> absurd
|
|
| FFalse -> absurd | PApp x0 x1 -> absurd
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_fo_formula v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_formula v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mv0 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
model_equal_fo_formula v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
let ghost mrv0 = rename_fo_formula mv0 identity identity in
|
|
let resv0 =
|
|
{ nlrepr_fo_formula_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field = fv1 ;
|
|
model_fo_formula_field = ghost mrv0 ;
|
|
}
|
|
in let res = NLC_Not resv0 in
|
|
free_var_equivalence_of_rename_fo_formula mv0 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y mv0 /\ eval (identity) y
|
|
= x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_formula x mrv0 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y mv0 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
| NL_FTrue ->
|
|
assert { t.model_fo_formula_field = FTrue } ;
|
|
let () =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> ()
|
|
| FFalse -> absurd | PApp x0 x1 -> absurd
|
|
end
|
|
in let res = NLC_FTrue in res
|
|
| NL_FFalse ->
|
|
assert { t.model_fo_formula_field = FFalse } ;
|
|
let () =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> absurd
|
|
| FFalse -> () | PApp x0 x1 -> absurd
|
|
end
|
|
in let res = NLC_FFalse in res
|
|
| NL_PApp v0 v1 ->
|
|
assert { t.model_fo_formula_field =
|
|
PApp
|
|
(nlmodel_symbol v0 (rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(nlmodel_fo_term_list v1
|
|
(rename_subst_symbol subst_id_symbol identity)
|
|
(rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity)
|
|
(rename_subst_fo_term subst_id_fo_term identity identity)
|
|
(rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
let (mv0 , mv1) =
|
|
match t.model_fo_formula_field with | Forall x0 -> absurd
|
|
| Exists x0 -> absurd | And x0 x1 -> absurd
|
|
| Or x0 x1 -> absurd | Not x0 -> absurd | FTrue -> absurd
|
|
| FFalse -> absurd | PApp x0 x1 -> (x0 , x1)
|
|
end
|
|
in
|
|
assert { mv0 =
|
|
nlmodel_symbol v0
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
} ;
|
|
assert { mv1 =
|
|
nlmodel_fo_term_list v1
|
|
((rename_subst_symbol subst_id_symbol identity))
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_symbol v0 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_symbol x mv0 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_symbol_in_fo_term_list v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_term_list x mv1 ->
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert { bound_depth_of_fo_term_in_fo_term_list v1 <= 0 } ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_term_list x mv1 ->
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field &&
|
|
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
model_equal_symbol v0 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity)) ;
|
|
model_equal_fo_term_list v1 subst_id_symbol
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
|
|
const (Var_symbol (-1)) : int -> (symbol int)))
|
|
(rename_subst_symbol
|
|
((rename_subst_symbol
|
|
(const (Var_symbol (-1)) : int -> (symbol int)) identity))
|
|
(identity))
|
|
subst_id_fo_term
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term subst_id_fo_term identity identity))
|
|
(identity) (identity)) ((const (Var_fo_term (-1)) :
|
|
int -> (fo_term int int)))
|
|
(rename_subst_fo_term
|
|
((rename_subst_fo_term
|
|
(const (Var_fo_term (-1)) : int -> (fo_term int int))
|
|
identity identity))
|
|
(identity) (identity)) ;
|
|
let ghost mrv0 = rename_symbol mv0 identity in
|
|
let ghost mrv1 = rename_fo_term_list mv1 identity identity in
|
|
let resv0 =
|
|
{ nlrepr_symbol_field = v0 ;
|
|
nlfree_var_symbol_set_abstraction_symbol_field = fv0 ;
|
|
model_symbol_field = ghost mrv0 ;
|
|
}
|
|
in
|
|
let resv1 =
|
|
{ nlrepr_fo_term_list_field = v1 ;
|
|
nlfree_var_symbol_set_abstraction_fo_term_list_field = fv0 ;
|
|
nlfree_var_fo_term_set_abstraction_fo_term_list_field = fv1 ;
|
|
model_fo_term_list_field = ghost mrv1 ;
|
|
}
|
|
in let res = NLC_PApp resv0 resv1 in
|
|
free_var_equivalence_of_rename_symbol mv0 (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
free_var_equivalence_of_rename_fo_term_list mv1 (identity)
|
|
(rcompose (identity) (identity)) (identity)
|
|
(rcompose (identity) (identity)) ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_symbol x mrv0 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_symbol y mv0 /\ eval (identity) y = x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_symbol_free_var_in_fo_term_list x mrv1 ->
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_term_list y mv1 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_symbol_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv0))
|
|
&& (x) < (fv0)
|
|
} ;
|
|
assert {
|
|
forall x:int. is_fo_term_free_var_in_fo_term_list x mrv1 ->
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_term_list y mv1 /\
|
|
eval (identity) y = x)
|
|
-> x = y &&
|
|
is_fo_term_free_var_in_fo_formula x t.model_fo_formula_field
|
|
&& (x) < (fv1))
|
|
&& (x) < (fv1)
|
|
} ;
|
|
res
|
|
end
|
|
|
|
let nlsubst_symbol_in_fo_formula (t:nlimpl_fo_formula) (x:int)
|
|
(u:nlimpl_symbol) : nlimpl_fo_formula requires { nlimpl_fo_formula_ok t }
|
|
requires { nlimpl_symbol_ok u } ensures { nlimpl_fo_formula_ok result }
|
|
ensures { result.model_fo_formula_field =
|
|
subst_fo_formula t.model_fo_formula_field
|
|
(update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
}
|
|
=
|
|
model_equal_fo_formula t.nlrepr_fo_formula_field
|
|
(subst_compose_symbol subst_id_symbol
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
(subst_compose_symbol (const (Var_symbol (-1)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)))
|
|
((const (Var_symbol (-1))))
|
|
(subst_compose_fo_term subst_id_fo_term
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
(subst_compose_fo_term (const (Var_fo_term (-1)))
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
|
|
((const (Var_fo_term (-1))));
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
subst_base_symbol_in_fo_formula t.nlrepr_fo_formula_field x
|
|
u.nlrepr_symbol_field (subst_id_symbol)
|
|
((const (Var_symbol (-1)))) (subst_id_fo_term)
|
|
((const (Var_fo_term (-1)))) ((const (Var_symbol (-1)))) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
(u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
t.nlfree_var_fo_term_set_abstraction_fo_formula_field ;
|
|
model_fo_formula_field = ghost
|
|
subst_fo_formula t.model_fo_formula_field
|
|
(update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field)
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int))) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x2:int.
|
|
is_symbol_free_var_in_fo_formula x2 res.model_fo_formula_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y t.model_fo_formula_field /\
|
|
is_symbol_free_var_in_symbol x2
|
|
(eval
|
|
((update (subst_id_symbol: (int) -> (symbol (int))) x
|
|
u.model_symbol_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field))
|
|
/\
|
|
(x <> y -> x2 = y && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field)))
|
|
&& (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field))
|
|
/\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y t.model_fo_formula_field
|
|
/\
|
|
is_symbol_free_var_in_fo_term x2
|
|
(eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
y))
|
|
-> false))
|
|
&& (x2) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x2:int.
|
|
is_fo_term_free_var_in_fo_formula x2 res.model_fo_formula_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y t.model_fo_formula_field
|
|
/\
|
|
is_fo_term_free_var_in_fo_term x2
|
|
(eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
|
|
y))
|
|
-> x2 = y && (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)))
|
|
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
res
|
|
|
|
let nlsubst_fo_term_in_fo_formula (t:nlimpl_fo_formula) (x:int)
|
|
(u:nlimpl_fo_term) : nlimpl_fo_formula
|
|
requires { nlimpl_fo_formula_ok t } requires { nlimpl_fo_term_ok u }
|
|
ensures { nlimpl_fo_formula_ok result }
|
|
ensures { result.model_fo_formula_field =
|
|
subst_fo_formula t.model_fo_formula_field
|
|
(subst_id_symbol: (int) -> (symbol (int)))
|
|
(update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)
|
|
}
|
|
=
|
|
model_equal_fo_formula t.nlrepr_fo_formula_field
|
|
(subst_compose_symbol subst_id_symbol
|
|
((subst_id_symbol: (int) -> (symbol (int)))))
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
(subst_compose_symbol (const (Var_symbol (-1)))
|
|
((subst_id_symbol: (int) -> (symbol (int)))))
|
|
((const (Var_symbol (-1))))
|
|
(subst_compose_fo_term subst_id_fo_term
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field))
|
|
(subst_compose_fo_term (const (Var_fo_term (-1)))
|
|
((subst_id_symbol: (int) -> (symbol (int))))
|
|
((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field)))
|
|
((const (Var_fo_term (-1))));
|
|
let res =
|
|
{
|
|
nlrepr_fo_formula_field =
|
|
subst_base_fo_term_in_fo_formula t.nlrepr_fo_formula_field x
|
|
u.nlrepr_fo_term_field (subst_id_symbol)
|
|
((const (Var_symbol (-1)))) (subst_id_fo_term)
|
|
((const (Var_fo_term (-1)))) ((const (Var_symbol (-1))))
|
|
((const (Var_fo_term (-1)))) ;
|
|
nlfree_var_symbol_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
(u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
|
|
nlfree_var_fo_term_set_abstraction_fo_formula_field =
|
|
(let aux (a:int) (b:int) : int
|
|
ensures { result >= a /\ result >= b } = if a < b then b else a
|
|
in
|
|
aux (t.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
(u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
|
|
model_fo_formula_field = ghost
|
|
subst_fo_formula t.model_fo_formula_field
|
|
(subst_id_symbol: (int) -> (symbol (int)))
|
|
(update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
|
|
u.model_fo_term_field) ;
|
|
}
|
|
in
|
|
assert {
|
|
forall x2:int.
|
|
is_symbol_free_var_in_fo_formula x2 res.model_fo_formula_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_symbol_free_var_in_fo_formula y t.model_fo_formula_field /\
|
|
is_symbol_free_var_in_symbol x2
|
|
(eval ((subst_id_symbol: (int) -> (symbol (int)))) y))
|
|
-> x2 = y && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field))
|
|
/\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y t.model_fo_formula_field
|
|
/\
|
|
is_symbol_free_var_in_fo_term x2
|
|
(eval
|
|
((update
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
x u.model_fo_term_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field))
|
|
/\ (x <> y -> false)) && (x2) <
|
|
(res.nlfree_var_symbol_set_abstraction_fo_formula_field)))
|
|
&& (x2) < (res.nlfree_var_symbol_set_abstraction_fo_formula_field)
|
|
} ;
|
|
assert {
|
|
forall x2:int.
|
|
is_fo_term_free_var_in_fo_formula x2 res.model_fo_formula_field ->
|
|
(true /\
|
|
(forall y:int.
|
|
(is_fo_term_free_var_in_fo_formula y t.model_fo_formula_field
|
|
/\
|
|
is_fo_term_free_var_in_fo_term x2
|
|
(eval
|
|
((update
|
|
(subst_id_fo_term: (int) -> (fo_term (int) (int)))
|
|
x u.model_fo_term_field))
|
|
y))
|
|
->
|
|
((x = y -> (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field))
|
|
/\
|
|
(x <> y -> x2 = y && (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)))
|
|
&& (x2) <
|
|
(res.nlfree_var_fo_term_set_abstraction_fo_formula_field)))
|
|
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_formula_field)
|
|
} ;
|
|
res
|
|
|
|
|
|
end
|