why3doc index index
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
Generated by why3doc 1.7.0