ada/why3
0
0
Fork 0
mirror of https://github.com/AdaCore/why3.git synced 2026-02-12 12:34:55 -08:00
Code Issues Packages Projects Releases Wiki Activity
Files
master
why3/examples/prover/Firstorder_term_impl.mlw
Andrei Paskevich eae547d95f stdlib, examples: remove redundant "import"
2018-06-15 16:45:58 +02:00

2643 lines
115 KiB
Plaintext
Raw Permalink Blame History

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
type nl_fo_term_list 'b0 'b3 =
| NL_FONil
| NL_FOCons (nl_fo_term 'b0 'b3) (nl_fo_term_list 'b0 'b3)
with nl_fo_term 'b0 'b3 =
| NLFVar_fo_term 'b3
| NLBruijn_fo_term int
| NL_App (nl_symbol 'b0) (nl_fo_term_list 'b0 'b3)
type nlimpl_fo_term_list =
{ nlrepr_fo_term_list_field : nl_fo_term_list int int ;
nlfree_var_symbol_set_abstraction_fo_term_list_field : int ;
nlfree_var_fo_term_set_abstraction_fo_term_list_field : int ;
ghost model_fo_term_list_field : fo_term_list int int ;
}
type nlimpl_fo_term =
{ nlrepr_fo_term_field : nl_fo_term int int ;
nlfree_var_symbol_set_abstraction_fo_term_field : int ;
nlfree_var_fo_term_set_abstraction_fo_term_field : int ;
ghost model_fo_term_field : fo_term int int ;
}
type cons_fo_term_list = | NLC_FONil
| NLC_FOCons (nlimpl_fo_term) (nlimpl_fo_term_list)
type cons_fo_term = | NLCVar_fo_term int
| NLC_App (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 Types
function nat_nlsize_fo_term_list (t:nl_fo_term_list 'b0 'b3) : nat =
match t with | NL_FONil -> let s = one_nat in s
| NL_FOCons 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_fo_term v0) s in s
end
with nat_nlsize_fo_term (t:nl_fo_term 'b0 'b3) : nat =
match t with | NLFVar_fo_term v0 -> one_nat
| NLBruijn_fo_term v0 -> one_nat
| NL_App 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_term_list (t:nl_fo_term_list 'b0 'b3) : int =
match t with | NL_FONil -> let s = 1 in s
| NL_FOCons v0 v1 ->
let s = 1 in let s = nlsize_fo_term_list v1 + s in
let s = nlsize_fo_term v0 + s in s
end
with nlsize_fo_term (t:nl_fo_term 'b0 'b3) : int =
match t with | NLFVar_fo_term v0 -> 1 | NLBruijn_fo_term v0 -> 1
| NL_App 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_term_list
(t:nl_fo_term_list 'b0 'b3) : unit ensures { nlsize_fo_term_list t > 0 }
variant { nat_to_int (nat_nlsize_fo_term_list t) } =
match t with | NL_FONil -> ()
| NL_FOCons v0 v1 ->
nlsize_positive_lemma_fo_term v0 ;
nlsize_positive_lemma_fo_term_list v1 ; ()
end
with lemma nlsize_positive_lemma_fo_term (t:nl_fo_term 'b0 'b3) : unit
ensures { nlsize_fo_term t > 0 }
variant { nat_to_int (nat_nlsize_fo_term t) } =
match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
| NL_App v0 v1 ->
nlsize_positive_lemma_symbol v0 ;
nlsize_positive_lemma_fo_term_list v1 ; ()
end
(* Abstraction definition axiom :
function shiftb_fo_term (bnd: int -> (fo_term 'b0 'b3)) :
int -> (fo_term 'b0 (option 'b3)) =
(\ i:int.
if i = 0 then Var_fo_term None
else rename_fo_term (bnd (i-1)) identity some)*)
function shiftb_fo_term (bnd: int -> (fo_term 'b0 'b3)) :
int -> (fo_term 'b0 (option 'b3))
axiom shiftb_fo_term_definition :
forall bnd: int -> (fo_term 'b0 'b3), i:int.
eval (shiftb_fo_term bnd) i =
if i = 0 then Var_fo_term None
else rename_fo_term (bnd (i-1)) identity some
let lemma shiftb_compose_lemma_fo_term (bnd: int -> (fo_term 'b0 'b3))
(s0:'b0 -> (symbol 'c0)) (s3:'b3 -> (fo_term 'c0 'c3)) : unit
ensures {
subst_compose_fo_term (shiftb_fo_term bnd)
(rename_subst_symbol s0 identity) (olifts_fo_term s3)
= shiftb_fo_term (subst_compose_fo_term bnd s0 s3) }
=
assert {
forall i:int. (i = 0 \/ i <> 0) ->
subst_fo_term (shiftb_fo_term bnd i)
(rename_subst_symbol s0 identity) (olifts_fo_term s3)
= eval (shiftb_fo_term (subst_compose_fo_term bnd s0 s3)) i
} ;
assert {
extensionalEqual
(subst_compose_fo_term (shiftb_fo_term bnd)
(rename_subst_symbol s0 identity) (olifts_fo_term s3))
(shiftb_fo_term (subst_compose_fo_term bnd s0 s3))
}
function nlmodel_fo_term_list (t:nl_fo_term_list 'b0 'b3)
(fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
(fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3)) :
fo_term_list 'c0 'c3 =
match t with | NL_FONil -> FONil
| NL_FOCons v0 v1 ->
FOCons
(nlmodel_fo_term v0 ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd0 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
(nlmodel_fo_term_list v1 ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd0 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
with nlmodel_fo_term (t:nl_fo_term 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
(bnd0: int -> (symbol 'c0)) (fr3:'b3 -> (fo_term 'c0 'c3))
(bnd3: int -> (fo_term 'c0 'c3)) : fo_term 'c0 'c3 =
match t with | NLFVar_fo_term v0 -> fr3 v0
| NLBruijn_fo_term v0 -> bnd3 v0
| NL_App v0 v1 ->
App
(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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
let rec lemma nlmodel_subst_commutation_lemma_fo_term_list
(t:nl_fo_term_list 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
(bnd0: int -> (symbol 'c0)) (s0:'c0 -> (symbol 'd0))
(fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
(s3:'c3 -> (fo_term 'd0 'd3)) : unit
ensures {
nlmodel_fo_term_list t (subst_compose_symbol fr0 s0)
(subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr3 s0 s3)
(subst_compose_fo_term bnd3 s0 s3)
= subst_fo_term_list (nlmodel_fo_term_list t fr0 bnd0 fr3 bnd3) s0 s3 }
variant { nlsize_fo_term_list t } =
match t with | NL_FONil -> ()
| NL_FOCons v0 v1 ->
nlmodel_subst_commutation_lemma_fo_term v0
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd0 identity))
((rename_subst_symbol s0 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity))
((rename_subst_fo_term s3 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 fr3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
identity)
} ;
assert {
subst_compose_fo_term
(rename_subst_fo_term bnd3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term bnd3 s0 s3)
identity 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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity))
((rename_subst_fo_term s3 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 fr3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
identity)
} ;
assert {
subst_compose_fo_term
(rename_subst_fo_term bnd3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term bnd3 s0 s3)
identity identity)
} ;
()
end
with lemma nlmodel_subst_commutation_lemma_fo_term (t:nl_fo_term 'b0 'b3)
(fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
(s0:'c0 -> (symbol 'd0)) (fr3:'b3 -> (fo_term 'c0 'c3))
(bnd3: int -> (fo_term 'c0 'c3)) (s3:'c3 -> (fo_term 'd0 'd3)) : unit
ensures {
nlmodel_fo_term t (subst_compose_symbol fr0 s0)
(subst_compose_symbol bnd0 s0) (subst_compose_fo_term fr3 s0 s3)
(subst_compose_fo_term bnd3 s0 s3)
= subst_fo_term (nlmodel_fo_term t fr0 bnd0 fr3 bnd3) s0 s3 }
variant { nlsize_fo_term t } =
match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
| NL_App 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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity))
((rename_subst_fo_term s3 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 fr3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term fr3 s0 s3) identity
identity)
} ;
assert {
subst_compose_fo_term
(rename_subst_fo_term bnd3 identity identity)
((rename_subst_symbol s0 identity))
((rename_subst_fo_term s3 identity identity))
=
(rename_subst_fo_term (subst_compose_fo_term bnd3 s0 s3)
identity identity)
} ;
()
end
let lemma nlmodel_rename_commutation_lemma_fo_term_list
(t:nl_fo_term_list 'b0 'b3) (fr0:'b0 -> (symbol 'c0))
(bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
(fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
(s3:'c3 -> 'd3) : unit
ensures {
nlmodel_fo_term_list t (rename_subst_symbol fr0 s0)
(rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr3 s0 s3)
(rename_subst_fo_term bnd3 s0 s3)
= rename_fo_term_list (nlmodel_fo_term_list t fr0 bnd0 fr3 bnd3) s0 s3
}
=
nlmodel_subst_commutation_lemma_fo_term_list t fr0 bnd0
(subst_of_rename_symbol s0) fr3 bnd3 (subst_of_rename_fo_term s3)
let lemma nlmodel_rename_commutation_lemma_fo_term (t:nl_fo_term 'b0 'b3)
(fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0)) (s0:'c0 -> 'd0)
(fr3:'b3 -> (fo_term 'c0 'c3)) (bnd3: int -> (fo_term 'c0 'c3))
(s3:'c3 -> 'd3) : unit
ensures {
nlmodel_fo_term t (rename_subst_symbol fr0 s0)
(rename_subst_symbol bnd0 s0) (rename_subst_fo_term fr3 s0 s3)
(rename_subst_fo_term bnd3 s0 s3)
= rename_fo_term (nlmodel_fo_term t fr0 bnd0 fr3 bnd3) s0 s3 }
=
nlmodel_subst_commutation_lemma_fo_term t fr0 bnd0
(subst_of_rename_symbol s0) fr3 bnd3 (subst_of_rename_fo_term s3)
predicate correct_indexes_fo_term_list (t:nl_fo_term_list 'b0 'b3) =
match t with | NL_FONil -> true
| NL_FOCons v0 v1 ->
correct_indexes_fo_term v0 /\ correct_indexes_fo_term_list v1
end
with correct_indexes_fo_term (t:nl_fo_term 'b0 'b3) =
match t with | NLFVar_fo_term v0 -> true | NLBruijn_fo_term v0 -> v0 >= 0
| NL_App v0 v1 ->
correct_indexes_symbol v0 /\ correct_indexes_fo_term_list v1
end
function bound_depth_of_symbol_in_fo_term_list
(t:nl_fo_term_list 'b0 'b3) : int =
match t with | NL_FONil -> 0
| NL_FOCons v0 v1 ->
let b = bound_depth_of_symbol_in_fo_term 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_term_list (t:nl_fo_term_list 'b0 'b3) :
int =
match t with | NL_FONil -> 0
| NL_FOCons v0 v1 ->
let b = bound_depth_of_fo_term_in_fo_term v0 in let a = b in
let b = bound_depth_of_fo_term_in_fo_term_list v1 in
let a = if a > b then a else b in a
end
with bound_depth_of_symbol_in_fo_term (t:nl_fo_term 'b0 'b3) : int =
match t with | NLFVar_fo_term v0 -> 0 | NLBruijn_fo_term v0 -> 0
| NL_App 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_term (t:nl_fo_term 'b0 'b3) : int =
match t with | NLFVar_fo_term v0 -> 0 | NLBruijn_fo_term v0 -> 1 + v0
| NL_App 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_term_list_nonnegative
(t:nl_fo_term_list 'b0 'b3) : unit
requires { correct_indexes_fo_term_list t }
ensures { bound_depth_of_symbol_in_fo_term_list t >= 0 }
variant { nlsize_fo_term_list t } =
match t with | NL_FONil -> ()
| NL_FOCons v0 v1 ->
bound_depth_of_symbol_in_fo_term_nonnegative v0 ;
bound_depth_of_symbol_in_fo_term_list_nonnegative v1 ; ()
end
with lemma bound_depth_of_fo_term_in_fo_term_list_nonnegative
(t:nl_fo_term_list 'b0 'b3) : unit
requires { correct_indexes_fo_term_list t }
ensures { bound_depth_of_fo_term_in_fo_term_list t >= 0 }
variant { nlsize_fo_term_list t } =
match t with | NL_FONil -> ()
| NL_FOCons v0 v1 ->
bound_depth_of_fo_term_in_fo_term_nonnegative v0 ;
bound_depth_of_fo_term_in_fo_term_list_nonnegative v1 ; ()
end
with lemma bound_depth_of_symbol_in_fo_term_nonnegative
(t:nl_fo_term 'b0 'b3) : unit requires { correct_indexes_fo_term t }
ensures { bound_depth_of_symbol_in_fo_term t >= 0 }
variant { nlsize_fo_term t } =
match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
| NL_App 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_term_nonnegative
(t:nl_fo_term 'b0 'b3) : unit requires { correct_indexes_fo_term t }
ensures { bound_depth_of_fo_term_in_fo_term t >= 0 }
variant { nlsize_fo_term t } =
match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
| NL_App v0 v1 ->
() ; bound_depth_of_fo_term_in_fo_term_list_nonnegative v1 ; ()
end
let rec lemma model_equal_fo_term_list (t:nl_fo_term_list 'b0 'b3)
(fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
(bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
(fr13: 'b3 -> (fo_term 'c0 'c3)) (fr23: 'b3 -> (fo_term 'c0 'c3))
(bnd13: int -> (fo_term 'c0 'c3)) (bnd23: int -> (fo_term 'c0 'c3)) :
unit
requires {
forall i:int. 0 <= i < bound_depth_of_symbol_in_fo_term_list t ->
bnd10 i = bnd20 i
}
requires { fr10 = fr20 }
requires {
forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_term_list t ->
bnd13 i = bnd23 i
}
requires { fr13 = fr23 } requires { correct_indexes_fo_term_list t }
ensures { nlmodel_fo_term_list t fr10 bnd10 fr13 bnd13 =
nlmodel_fo_term_list t fr20 bnd20 fr23 bnd23 }
variant { nlsize_fo_term_list t } =
match t with | NL_FONil -> ()
| NL_FOCons v0 v1 ->
model_equal_fo_term 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 fr13 identity identity))
((rename_subst_fo_term fr23 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_fo_term bnd23 identity 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 fr13 identity identity))
((rename_subst_fo_term fr23 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_fo_term bnd23 identity identity)) ;
()
end
with lemma model_equal_fo_term (t:nl_fo_term 'b0 'b3)
(fr10: 'b0 -> (symbol 'c0)) (fr20: 'b0 -> (symbol 'c0))
(bnd10: int -> (symbol 'c0)) (bnd20: int -> (symbol 'c0))
(fr13: 'b3 -> (fo_term 'c0 'c3)) (fr23: 'b3 -> (fo_term 'c0 'c3))
(bnd13: int -> (fo_term 'c0 'c3)) (bnd23: int -> (fo_term 'c0 'c3)) :
unit
requires {
forall i:int. 0 <= i < bound_depth_of_symbol_in_fo_term t -> bnd10 i =
bnd20 i
}
requires { fr10 = fr20 }
requires {
forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_term t -> bnd13 i
= bnd23 i
}
requires { fr13 = fr23 } requires { correct_indexes_fo_term t }
ensures { nlmodel_fo_term t fr10 bnd10 fr13 bnd13 =
nlmodel_fo_term t fr20 bnd20 fr23 bnd23 }
variant { nlsize_fo_term t } =
match t with | NLFVar_fo_term v0 -> () | NLBruijn_fo_term v0 -> ()
| NL_App 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 fr13 identity identity))
((rename_subst_fo_term fr23 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_fo_term bnd23 identity identity)) ;
()
end
predicate nlimpl_fo_term_list_ok (t:nlimpl_fo_term_list) =
nlmodel_fo_term_list t.nlrepr_fo_term_list_field subst_id_symbol
(const (Var_symbol ((-1)))) subst_id_fo_term
(const (Var_fo_term ((-1)))) = t.model_fo_term_list_field
/\ correct_indexes_fo_term_list t.nlrepr_fo_term_list_field /\
bound_depth_of_symbol_in_fo_term_list t.nlrepr_fo_term_list_field = 0 /\
bound_depth_of_fo_term_in_fo_term_list t.nlrepr_fo_term_list_field = 0 /\
(forall x:int.
is_symbol_free_var_in_fo_term_list x t.model_fo_term_list_field -> (x)
< (t.nlfree_var_symbol_set_abstraction_fo_term_list_field))
/\
(forall x:int.
is_fo_term_free_var_in_fo_term_list x t.model_fo_term_list_field ->
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_term_list_field))
predicate nlimpl_fo_term_ok (t:nlimpl_fo_term) =
nlmodel_fo_term t.nlrepr_fo_term_field subst_id_symbol
(const (Var_symbol ((-1)))) subst_id_fo_term
(const (Var_fo_term ((-1)))) = t.model_fo_term_field
/\ correct_indexes_fo_term t.nlrepr_fo_term_field /\
bound_depth_of_symbol_in_fo_term t.nlrepr_fo_term_field = 0 /\
bound_depth_of_fo_term_in_fo_term t.nlrepr_fo_term_field = 0 /\
(forall x:int. is_symbol_free_var_in_fo_term x t.model_fo_term_field ->
(x) < (t.nlfree_var_symbol_set_abstraction_fo_term_field))
/\
(forall x:int. is_fo_term_free_var_in_fo_term x t.model_fo_term_field ->
(x) < (t.nlfree_var_fo_term_set_abstraction_fo_term_field))
predicate cons_ok_fo_term_list (c:cons_fo_term_list) =
match c with | NLC_FONil -> true
| NLC_FOCons v0 v1 -> nlimpl_fo_term_ok v0 /\ nlimpl_fo_term_list_ok v1
end
predicate cons_ok_fo_term (c:cons_fo_term) =
match c with | NLCVar_fo_term v0 -> true
| NLC_App v0 v1 -> nlimpl_symbol_ok v0 /\ nlimpl_fo_term_list_ok v1
end
predicate cons_rel_fo_term_list (c:cons_fo_term_list)
(t:nlimpl_fo_term_list) =
match c with | NLC_FONil -> t.model_fo_term_list_field = FONil
| NLC_FOCons v0 v1 -> t.model_fo_term_list_field =
FOCons (rename_fo_term v0.model_fo_term_field identity identity)
(rename_fo_term_list v1.model_fo_term_list_field identity identity)
end
predicate cons_rel_fo_term (c:cons_fo_term) (t:nlimpl_fo_term) =
match c with
| NLCVar_fo_term v0 -> t.model_fo_term_field = Var_fo_term v0
| NLC_App v0 v1 -> t.model_fo_term_field =
App (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_term_list (c:cons_fo_term_list)
(t:nlimpl_fo_term_list) =
match c with
| NLC_FONil ->
match t.model_fo_term_list_field with | FONil -> true
| FOCons w0 w1 -> false
end
| NLC_FOCons v0 v1 ->
match t.model_fo_term_list_field with | FONil -> false
| FOCons w0 w1 ->
v0.model_fo_term_field = (rename_fo_term w0 identity identity) /\
v1.model_fo_term_list_field =
(rename_fo_term_list w1 identity identity)
end
end
predicate cons_open_rel_fo_term (c:cons_fo_term) (t:nlimpl_fo_term) =
match c with
| NLCVar_fo_term v0 -> t.model_fo_term_field = Var_fo_term v0
| NLC_App v0 v1 ->
match t.model_fo_term_field with | Var_fo_term w0 -> false
| App 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 Types
use Logic
let rec bind_var_symbol_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
(i:int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd0: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
requires { correct_indexes_fo_term_list t }
requires { bound_depth_of_symbol_in_fo_term_list t <= i }
variant { nlsize_fo_term_list t }
ensures { bound_depth_of_symbol_in_fo_term_list result <= i + 1 }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_fo_term_in_fo_term_list t =
bound_depth_of_fo_term_in_fo_term_list result }
ensures { nlmodel_fo_term_list result fr0 bnd0 fr3 bnd3 =
nlmodel_fo_term_list t (update fr0 x (bnd0 i)) bnd0 fr3 bnd3 }
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons 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_FOCons
(bind_var_symbol_in_fo_term v0 x (i+0)
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd0 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd3 identity 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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
with bind_var_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
(i:int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd0: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
requires { correct_indexes_fo_term_list t }
requires { bound_depth_of_fo_term_in_fo_term_list t <= i }
variant { nlsize_fo_term_list t }
ensures { bound_depth_of_fo_term_in_fo_term_list result <= i + 1 }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_symbol_in_fo_term_list t =
bound_depth_of_symbol_in_fo_term_list result }
ensures { nlmodel_fo_term_list result fr0 bnd0 fr3 bnd3 =
nlmodel_fo_term_list t fr0 bnd0 (update fr3 x (bnd3 i)) bnd3 }
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons v0 v1 ->
assert { (rename_fo_term (bnd3 i) identity identity) =
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
assert {
extensionalEqual
((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
identity))
((update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (bnd3 i) identity identity)))
};
assert {
(rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
=
(update ((rename_subst_fo_term fr3 identity identity)) x
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
};
assert { (rename_fo_term (bnd3 i) identity identity) =
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
assert {
extensionalEqual
((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
identity))
((update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (bnd3 i) identity identity)))
};
assert {
(rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
=
(update ((rename_subst_fo_term fr3 identity identity)) x
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
};
NL_FOCons
(bind_var_fo_term_in_fo_term v0 x (i+0)
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd0 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
(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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
with bind_var_symbol_in_fo_term (t:nl_fo_term int int) (x:int) (i:int)
(ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
(ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
requires { correct_indexes_fo_term t }
requires { bound_depth_of_symbol_in_fo_term t <= i }
variant { nlsize_fo_term t }
ensures { bound_depth_of_symbol_in_fo_term result <= i + 1 }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_fo_term_in_fo_term t =
bound_depth_of_fo_term_in_fo_term result }
ensures { nlmodel_fo_term result fr0 bnd0 fr3 bnd3 =
nlmodel_fo_term t (update fr0 x (bnd0 i)) bnd0 fr3 bnd3 }
=
match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
| NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
| NL_App 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_App
(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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
with bind_var_fo_term_in_fo_term (t:nl_fo_term int int) (x:int) (i:int)
(ghost fr0: int -> (symbol 'b0)) (ghost bnd0: int -> (symbol 'b0))
(ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd3: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
requires { correct_indexes_fo_term t }
requires { bound_depth_of_fo_term_in_fo_term t <= i }
variant { nlsize_fo_term t }
ensures { bound_depth_of_fo_term_in_fo_term result <= i + 1 }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_symbol_in_fo_term t =
bound_depth_of_symbol_in_fo_term result }
ensures { nlmodel_fo_term result fr0 bnd0 fr3 bnd3 =
nlmodel_fo_term t fr0 bnd0 (update fr3 x (bnd3 i)) bnd3 }
=
match t with
| NLFVar_fo_term v0 ->
if v0 = x then NLBruijn_fo_term i else NLFVar_fo_term v0
| NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
| NL_App v0 v1 ->
assert { (rename_fo_term (bnd3 i) identity identity) =
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)) };
assert {
extensionalEqual
((rename_subst_fo_term (update fr3 x (bnd3 i)) identity
identity))
((update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (bnd3 i) identity identity)))
};
assert {
(rename_subst_fo_term (update fr3 x (bnd3 i)) identity identity)
=
(update ((rename_subst_fo_term fr3 identity identity)) x
(eval ((rename_subst_fo_term bnd3 identity identity)) (i+0)))
};
NL_App (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 fr3 identity identity))
((rename_subst_fo_term bnd3 identity identity)))
end
let rec unbind_var_symbol_in_fo_term_list (t:nl_fo_term_list int int)
(i:int) (x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_term_list int int
requires { i >= 0 } requires { correct_indexes_fo_term_list t }
requires { bound_depth_of_symbol_in_fo_term_list t <= i + 1 }
requires { correct_indexes_symbol x }
requires { bound_depth_of_symbol_in_symbol x = 0 }
variant { nlsize_fo_term_list t }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_symbol_in_fo_term_list result <= i }
ensures { bound_depth_of_fo_term_in_fo_term_list result =
bound_depth_of_fo_term_in_fo_term_list t }
ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term_list t fr0
(update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr3 bnd13
}
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons 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_FOCons
(unbind_var_symbol_in_fo_term v0 (i+0) x
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd10 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd13 identity 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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity)))
end
with unbind_var_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (i:int)
(x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0))
(ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
requires { i >= 0 } requires { correct_indexes_fo_term_list t }
requires { bound_depth_of_fo_term_in_fo_term_list 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_term_list t }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_fo_term_in_fo_term_list result <= i }
ensures { bound_depth_of_symbol_in_fo_term_list result =
bound_depth_of_symbol_in_fo_term_list t }
ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term_list t fr0 bnd10 fr3
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
}
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons v0 v1 ->
assert {
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity)
=
update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
assert {
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity)
=
update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
NL_FOCons
(unbind_var_fo_term_in_fo_term v0 (i+0) x
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd10 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
(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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
end
with unbind_var_symbol_in_fo_term (t:nl_fo_term int int) (i:int)
(x:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_term int int
requires { i >= 0 } requires { correct_indexes_fo_term t }
requires { bound_depth_of_symbol_in_fo_term t <= i + 1 }
requires { correct_indexes_symbol x }
requires { bound_depth_of_symbol_in_symbol x = 0 }
variant { nlsize_fo_term t }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_symbol_in_fo_term result <= i }
ensures { bound_depth_of_fo_term_in_fo_term result =
bound_depth_of_fo_term_in_fo_term t }
ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term t fr0 (update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr3
bnd13
}
=
match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
| NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
| NL_App 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_App
(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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity)))
end
with unbind_var_fo_term_in_fo_term (t:nl_fo_term int int) (i:int)
(x:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0))
(ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
requires { i >= 0 } requires { correct_indexes_fo_term t }
requires { bound_depth_of_fo_term_in_fo_term 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_term t }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_fo_term_in_fo_term result <= i }
ensures { bound_depth_of_symbol_in_fo_term result =
bound_depth_of_symbol_in_fo_term t }
ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term t fr0 bnd10 fr3
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
}
=
match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
| NLBruijn_fo_term v0 ->
if v0 = i
then (model_equal_fo_term x fr0 fr0 bnd10 bnd20 fr3 fr3 bnd13 bnd23 ;
x)
else NLBruijn_fo_term v0
| NL_App v0 v1 ->
assert {
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity)
=
update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
assert {
rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(rename_fo_term (nlmodel_fo_term x fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update bnd13 i (nlmodel_fo_term x fr0 bnd20 fr3 bnd23))
identity identity)
=
update ((rename_subst_fo_term bnd13 identity identity)) (i+0)
(nlmodel_fo_term x ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
NL_App (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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
end
let rec subst_base_symbol_in_fo_term_list (t:nl_fo_term_list int int)
(x:int) (u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_term_list int int
requires { correct_indexes_fo_term_list t }
requires { correct_indexes_symbol u }
requires { bound_depth_of_symbol_in_symbol u = 0 }
variant { nlsize_fo_term_list t }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_symbol_in_fo_term_list result =
bound_depth_of_symbol_in_fo_term_list t }
ensures { bound_depth_of_fo_term_in_fo_term_list result =
bound_depth_of_fo_term_in_fo_term_list t }
ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term_list t (update fr0 x (nlmodel_symbol u fr0 bnd20))
bnd10 fr3 bnd13
}
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons 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_FOCons
(subst_base_symbol_in_fo_term v0 x u
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd10 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd13 identity 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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity)))
end
with subst_base_fo_term_in_fo_term_list (t:nl_fo_term_list int int) (x:int)
(u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0))
(ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term_list int int
requires { correct_indexes_fo_term_list 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_term_list t }
ensures { correct_indexes_fo_term_list result }
ensures { bound_depth_of_symbol_in_fo_term_list result =
bound_depth_of_symbol_in_fo_term_list t }
ensures { bound_depth_of_fo_term_in_fo_term_list result =
bound_depth_of_fo_term_in_fo_term_list t }
ensures { nlmodel_fo_term_list result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term_list t fr0 bnd10
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) bnd13
}
=
match t with | NL_FONil -> NL_FONil
| NL_FOCons v0 v1 ->
assert {
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
identity)
=
update ((rename_subst_fo_term fr3 identity identity)) x
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
assert {
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
identity)
=
update ((rename_subst_fo_term fr3 identity identity)) x
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
NL_FOCons
(subst_base_fo_term_in_fo_term v0 x u
((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd10 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
(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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
end
with subst_base_symbol_in_fo_term (t:nl_fo_term int int) (x:int)
(u:nl_symbol int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0)) : nl_fo_term int int
requires { correct_indexes_fo_term t }
requires { correct_indexes_symbol u }
requires { bound_depth_of_symbol_in_symbol u = 0 }
variant { nlsize_fo_term t }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_symbol_in_fo_term result =
bound_depth_of_symbol_in_fo_term t }
ensures { bound_depth_of_fo_term_in_fo_term result =
bound_depth_of_fo_term_in_fo_term t }
ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term t (update fr0 x (nlmodel_symbol u fr0 bnd20)) bnd10 fr3
bnd13
}
=
match t with | NLFVar_fo_term v0 -> NLFVar_fo_term v0
| NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
| NL_App 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_App
(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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity)))
end
with subst_base_fo_term_in_fo_term (t:nl_fo_term int int) (x:int)
(u:nl_fo_term int int) (ghost fr0: int -> (symbol 'b0))
(ghost bnd10: int -> (symbol 'b0)) (ghost fr3: int -> (fo_term 'b0 'b3))
(ghost bnd13: int -> (fo_term 'b0 'b3))
(ghost bnd20: int -> (symbol 'b0))
(ghost bnd23: int -> (fo_term 'b0 'b3)) : nl_fo_term int int
requires { correct_indexes_fo_term 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_term t }
ensures { correct_indexes_fo_term result }
ensures { bound_depth_of_symbol_in_fo_term result =
bound_depth_of_symbol_in_fo_term t }
ensures { bound_depth_of_fo_term_in_fo_term result =
bound_depth_of_fo_term_in_fo_term t }
ensures { nlmodel_fo_term result fr0 bnd10 fr3 bnd13 =
nlmodel_fo_term t fr0 bnd10
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) bnd13
}
=
match t with
| NLFVar_fo_term v0 ->
if v0 = x
then (model_equal_fo_term u fr0 fr0 bnd10 bnd20 fr3 fr3 bnd13 bnd23 ;
u)
else NLFVar_fo_term v0
| NLBruijn_fo_term v0 -> NLBruijn_fo_term v0
| NL_App v0 v1 ->
assert {
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
identity)
=
update ((rename_subst_fo_term fr3 identity identity)) x
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
assert {
rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23) identity
identity
=
nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity))
} ;
assert {
extensionalEqual
((rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23))
identity identity))
(update ((rename_subst_fo_term fr3 identity identity)) x
(rename_fo_term (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)
identity identity))
} ;
assert {
(rename_subst_fo_term
(update fr3 x (nlmodel_fo_term u fr0 bnd20 fr3 bnd23)) identity
identity)
=
update ((rename_subst_fo_term fr3 identity identity)) x
(nlmodel_fo_term u ((rename_subst_symbol fr0 identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term fr3 identity identity))
((rename_subst_fo_term bnd23 identity identity)))
} ;
NL_App (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 fr3 identity identity))
((rename_subst_fo_term bnd13 identity identity))
((rename_subst_symbol bnd20 identity))
((rename_subst_fo_term bnd23 identity identity)))
end
let construct_fo_term_list (c:cons_fo_term_list) : nlimpl_fo_term_list
requires { cons_ok_fo_term_list c }
ensures { nlimpl_fo_term_list_ok result }
ensures { cons_rel_fo_term_list c result }
(*ensures { cons_open_rel_fo_term_list c result }*) =
match c with
| NLC_FONil ->
let res =
{ nlrepr_fo_term_list_field = (NL_FONil) ;
nlfree_var_symbol_set_abstraction_fo_term_list_field = 0 ;
nlfree_var_fo_term_set_abstraction_fo_term_list_field = 0 ;
model_fo_term_list_field = ghost (FONil) ;
}
in
assert {
forall x:int.
is_symbol_free_var_in_fo_term_list x res.model_fo_term_list_field
-> (false) && (x) <
(res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
} ;
assert {
forall x:int.
is_fo_term_free_var_in_fo_term_list x
res.model_fo_term_list_field
-> (false) && (x) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
} ;
res
| NLC_FOCons v0 v1 -> assert { nlimpl_fo_term_ok v0 } ;
assert { nlimpl_fo_term_list_ok v1 } ;
let res =
{
nlrepr_fo_term_list_field =
(NL_FOCons (let v0 = v0.nlrepr_fo_term_field in v0)
(let v1 = v1.nlrepr_fo_term_list_field in v1)) ;
nlfree_var_symbol_set_abstraction_fo_term_list_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_term_field)
(v1.nlfree_var_symbol_set_abstraction_fo_term_list_field)) ;
nlfree_var_fo_term_set_abstraction_fo_term_list_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_term_field)
(v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field)) ;
model_fo_term_list_field = ghost
(FOCons
(rename_fo_term v0.model_fo_term_field identity identity)
(rename_fo_term_list v1.model_fo_term_list_field identity
identity)) ;
}
in
assert {
forall x:int.
is_symbol_free_var_in_fo_term x
(rename_fo_term v0.model_fo_term_field identity identity)
->
(forall y:int.
(is_symbol_free_var_in_fo_term y v0.model_fo_term_field /\
eval (identity) y = x) -> x = eval (identity) y && x = y &&
is_symbol_free_var_in_fo_term x v0.model_fo_term_field)
&& is_symbol_free_var_in_fo_term x v0.model_fo_term_field && (x)
< (v0.nlfree_var_symbol_set_abstraction_fo_term_field) && (x) <
(res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
} ;
assert {
forall x:int.
is_fo_term_free_var_in_fo_term x
(rename_fo_term v0.model_fo_term_field identity identity)
->
(forall y:int.
(is_fo_term_free_var_in_fo_term y v0.model_fo_term_field /\
eval (identity) y = x) -> x = eval (identity) y && x = y &&
is_fo_term_free_var_in_fo_term x v0.model_fo_term_field)
&& is_fo_term_free_var_in_fo_term x v0.model_fo_term_field && (x)
< (v0.nlfree_var_fo_term_set_abstraction_fo_term_field) && (x) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_list_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_term_list_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_term_list_field)
} ;
assert {
forall x:int.
is_symbol_free_var_in_fo_term_list x res.model_fo_term_list_field
->
(is_symbol_free_var_in_fo_term x
(rename_fo_term v0.model_fo_term_field identity 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_term_list_field)
} ;
assert {
forall x:int.
is_fo_term_free_var_in_fo_term_list x
res.model_fo_term_list_field
->
(is_fo_term_free_var_in_fo_term x
(rename_fo_term v0.model_fo_term_field identity identity) \/
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_term_list_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_term v0.nlrepr_fo_term_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_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 construct_fo_term (c:cons_fo_term) : nlimpl_fo_term
requires { cons_ok_fo_term c } ensures { nlimpl_fo_term_ok result }
ensures { cons_rel_fo_term c result }
(*ensures { cons_open_rel_fo_term c result }*) =
match c with
| NLCVar_fo_term v0 ->
{ nlrepr_fo_term_field = NLFVar_fo_term v0 ;
nlfree_var_symbol_set_abstraction_fo_term_field = 0 ;
nlfree_var_fo_term_set_abstraction_fo_term_field = (1 + (v0)) ;
model_fo_term_field = ghost (Var_fo_term v0) ;
}
| NLC_App v0 v1 -> assert { nlimpl_symbol_ok v0 } ;
assert { nlimpl_fo_term_list_ok v1 } ;
let res =
{
nlrepr_fo_term_field =
(NL_App (let v0 = v0.nlrepr_symbol_field in v0)
(let v1 = v1.nlrepr_fo_term_list_field in v1)) ;
nlfree_var_symbol_set_abstraction_fo_term_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_term_field =
v1.nlfree_var_fo_term_set_abstraction_fo_term_list_field ;
model_fo_term_field = ghost
(App (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_term_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_term_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_term_field)
} ;
assert {
forall x:int.
is_symbol_free_var_in_fo_term x res.model_fo_term_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_term_field)
} ;
assert {
forall x:int.
is_fo_term_free_var_in_fo_term x res.model_fo_term_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_term_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_term_list (t:nlimpl_fo_term_list) : cons_fo_term_list
requires { nlimpl_fo_term_list_ok t }
ensures { cons_ok_fo_term_list result }
ensures { cons_rel_fo_term_list result t }
ensures { cons_open_rel_fo_term_list result t } =
let fv0 = t.nlfree_var_symbol_set_abstraction_fo_term_list_field in
let fv3 = t.nlfree_var_fo_term_set_abstraction_fo_term_list_field in
match t.nlrepr_fo_term_list_field with
| NL_FONil ->
assert { t.model_fo_term_list_field = FONil } ;
let () =
match t.model_fo_term_list_field with | FONil -> ()
| FOCons x0 x1 -> absurd
end
in let res = NLC_FONil in res
| NL_FOCons v0 v1 ->
assert { t.model_fo_term_list_field =
FOCons
(nlmodel_fo_term 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_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_term_list_field with | FONil -> absurd
| FOCons x0 x1 -> (x0 , x1)
end
in
assert { mv0 =
nlmodel_fo_term 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_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_fo_term v0 <= 0 } ;
assert {
forall x:int. is_symbol_free_var_in_fo_term x mv0 ->
is_symbol_free_var_in_fo_term_list x t.model_fo_term_list_field
&& (x) <
(t.nlfree_var_symbol_set_abstraction_fo_term_list_field)
} ;
assert { bound_depth_of_fo_term_in_fo_term v0 <= 0 } ;
assert {
forall x:int. is_fo_term_free_var_in_fo_term x mv0 ->
is_fo_term_free_var_in_fo_term_list x
t.model_fo_term_list_field
&& (x) <
(t.nlfree_var_fo_term_set_abstraction_fo_term_list_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_term_list x t.model_fo_term_list_field
&& (x) <
(t.nlfree_var_symbol_set_abstraction_fo_term_list_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_term_list x
t.model_fo_term_list_field
&& (x) <
(t.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
} ;
model_equal_fo_term 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_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_fo_term mv0 identity identity in
let ghost mrv1 = rename_fo_term_list mv1 identity identity in
let resv0 =
{ nlrepr_fo_term_field = v0 ;
nlfree_var_symbol_set_abstraction_fo_term_field = fv0 ;
nlfree_var_fo_term_set_abstraction_fo_term_field = fv3 ;
model_fo_term_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 = fv3 ;
model_fo_term_list_field = ghost mrv1 ;
}
in let res = NLC_FOCons resv0 resv1 in
free_var_equivalence_of_rename_fo_term mv0 (identity)
(rcompose (identity) (identity)) (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_fo_term x mrv0 ->
(forall y:int.
(is_symbol_free_var_in_fo_term y mv0 /\ eval (identity) y =
x)
-> x = y &&
is_symbol_free_var_in_fo_term_list x
t.model_fo_term_list_field
&& (x) < (fv0))
&& (x) < (fv0)
} ;
assert {
forall x:int. is_fo_term_free_var_in_fo_term x mrv0 ->
(forall y:int.
(is_fo_term_free_var_in_fo_term y mv0 /\ eval (identity) y =
x)
-> x = y &&
is_fo_term_free_var_in_fo_term_list x
t.model_fo_term_list_field
&& (x) < (fv3))
&& (x) < (fv3)
} ;
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_term_list x
t.model_fo_term_list_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_term_list x
t.model_fo_term_list_field
&& (x) < (fv3))
&& (x) < (fv3)
} ;
res
end
let destruct_fo_term (t:nlimpl_fo_term) : cons_fo_term
requires { nlimpl_fo_term_ok t } ensures { cons_ok_fo_term result }
ensures { cons_rel_fo_term result t }
ensures { cons_open_rel_fo_term result t } =
let fv0 = t.nlfree_var_symbol_set_abstraction_fo_term_field in
let fv3 = t.nlfree_var_fo_term_set_abstraction_fo_term_field in
match t.nlrepr_fo_term_field with
| NLFVar_fo_term v0 -> NLCVar_fo_term v0
| NLBruijn_fo_term v0 -> absurd
| NL_App v0 v1 ->
assert { t.model_fo_term_field =
App
(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_term_field with | Var_fo_term x0 -> absurd
| App 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_term x t.model_fo_term_field && (x) <
(t.nlfree_var_symbol_set_abstraction_fo_term_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_term x t.model_fo_term_field && (x) <
(t.nlfree_var_symbol_set_abstraction_fo_term_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_term x t.model_fo_term_field && (x) <
(t.nlfree_var_fo_term_set_abstraction_fo_term_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 = fv3 ;
model_fo_term_list_field = ghost mrv1 ;
}
in let res = NLC_App 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_term x t.model_fo_term_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_term x t.model_fo_term_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_term x t.model_fo_term_field &&
(x) < (fv3))
&& (x) < (fv3)
} ;
res
end
let nlsubst_symbol_in_fo_term_list (t:nlimpl_fo_term_list) (x:int)
(u:nlimpl_symbol) : nlimpl_fo_term_list
requires { nlimpl_fo_term_list_ok t } requires { nlimpl_symbol_ok u }
ensures { nlimpl_fo_term_list_ok result }
ensures { result.model_fo_term_list_field =
subst_fo_term_list t.model_fo_term_list_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_term_list t.nlrepr_fo_term_list_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_term_list_field =
subst_base_symbol_in_fo_term_list t.nlrepr_fo_term_list_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_term_list_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_term_list_field)
(u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
nlfree_var_fo_term_set_abstraction_fo_term_list_field =
t.nlfree_var_fo_term_set_abstraction_fo_term_list_field ;
model_fo_term_list_field = ghost
subst_fo_term_list t.model_fo_term_list_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_term_list x2 res.model_fo_term_list_field ->
(true /\
(forall y:int.
(is_symbol_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field))
/\
(x <> y -> x2 = y && (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_list_field)))
&& (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_list_field))
/\
(forall y:int.
(is_fo_term_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field)
} ;
assert {
forall x2:int.
is_fo_term_free_var_in_fo_term_list x2 res.model_fo_term_list_field
->
(true /\
(forall y:int.
(is_fo_term_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field)))
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
} ;
res
let nlsubst_fo_term_in_fo_term_list (t:nlimpl_fo_term_list) (x:int)
(u:nlimpl_fo_term) : nlimpl_fo_term_list
requires { nlimpl_fo_term_list_ok t } requires { nlimpl_fo_term_ok u }
ensures { nlimpl_fo_term_list_ok result }
ensures { result.model_fo_term_list_field =
subst_fo_term_list t.model_fo_term_list_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_term_list t.nlrepr_fo_term_list_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_term_list_field =
subst_base_fo_term_in_fo_term_list t.nlrepr_fo_term_list_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_term_list_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_term_list_field)
(u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
nlfree_var_fo_term_set_abstraction_fo_term_list_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_term_list_field)
(u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
model_fo_term_list_field = ghost
subst_fo_term_list t.model_fo_term_list_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_term_list x2 res.model_fo_term_list_field ->
(true /\
(forall y:int.
(is_symbol_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field))
/\
(forall y:int.
(is_fo_term_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field))
/\ (x <> y -> false)) && (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_list_field)))
&& (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_list_field)
} ;
assert {
forall x2:int.
is_fo_term_free_var_in_fo_term_list x2 res.model_fo_term_list_field
->
(true /\
(forall y:int.
(is_fo_term_free_var_in_fo_term_list y
t.model_fo_term_list_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_term_list_field))
/\
(x <> y -> x2 = y && (x2) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)))
&& (x2) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)))
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_list_field)
} ;
res
let nlsubst_symbol_in_fo_term (t:nlimpl_fo_term) (x:int)
(u:nlimpl_symbol) : nlimpl_fo_term requires { nlimpl_fo_term_ok t }
requires { nlimpl_symbol_ok u } ensures { nlimpl_fo_term_ok result }
ensures { result.model_fo_term_field =
subst_fo_term t.model_fo_term_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_term t.nlrepr_fo_term_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_term_field =
subst_base_symbol_in_fo_term t.nlrepr_fo_term_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_term_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_term_field)
(u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
nlfree_var_fo_term_set_abstraction_fo_term_field =
t.nlfree_var_fo_term_set_abstraction_fo_term_field ;
model_fo_term_field = ghost
subst_fo_term t.model_fo_term_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_term x2 res.model_fo_term_field
->
(true /\
(forall y:int.
(is_symbol_free_var_in_fo_term y t.model_fo_term_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_term_field))
/\
(x <> y -> x2 = y && (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_field)))
&& (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_field))
/\
(forall y:int.
(is_fo_term_free_var_in_fo_term y t.model_fo_term_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_term_field)
} ;
assert {
forall x2:int.
is_fo_term_free_var_in_fo_term x2 res.model_fo_term_field ->
(true /\
(forall y:int.
(is_fo_term_free_var_in_fo_term y t.model_fo_term_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_term_field)))
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
} ;
res
let nlsubst_fo_term_in_fo_term (t:nlimpl_fo_term) (x:int)
(u:nlimpl_fo_term) : nlimpl_fo_term requires { nlimpl_fo_term_ok t }
requires { nlimpl_fo_term_ok u } ensures { nlimpl_fo_term_ok result }
ensures { result.model_fo_term_field =
subst_fo_term t.model_fo_term_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_term t.nlrepr_fo_term_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_term_field =
subst_base_fo_term_in_fo_term t.nlrepr_fo_term_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_term_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_term_field)
(u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
nlfree_var_fo_term_set_abstraction_fo_term_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_term_field)
(u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
model_fo_term_field = ghost
subst_fo_term t.model_fo_term_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_term x2 res.model_fo_term_field
->
(true /\
(forall y:int.
(is_symbol_free_var_in_fo_term y t.model_fo_term_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_term_field))
/\
(forall y:int.
(is_fo_term_free_var_in_fo_term y t.model_fo_term_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_term_field))
/\ (x <> y -> false)) && (x2) <
(res.nlfree_var_symbol_set_abstraction_fo_term_field)))
&& (x2) < (res.nlfree_var_symbol_set_abstraction_fo_term_field)
} ;
assert {
forall x2:int.
is_fo_term_free_var_in_fo_term x2 res.model_fo_term_field ->
(true /\
(forall y:int.
(is_fo_term_free_var_in_fo_term y t.model_fo_term_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_term_field))
/\
(x <> y -> x2 = y && (x2) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_field)))
&& (x2) <
(res.nlfree_var_fo_term_set_abstraction_fo_term_field)))
&& (x2) < (res.nlfree_var_fo_term_set_abstraction_fo_term_field)
} ;
res
end
Reference in New Issue View Git Blame Copy Permalink