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
  use Firstorder_formula_impl.Types
  use Firstorder_formula_impl.Logic
  use Firstorder_formula_impl.Impl
  use Firstorder_formula_list_spec.Spec
  type nl_fo_formula_list 'b0 'b1 =
    | NL_FOFNil
    | NL_FOFCons (nl_fo_formula 'b0 'b1) (nl_fo_formula_list 'b0 'b1)

  type nlimpl_fo_formula_list =
    { nlrepr_fo_formula_list_field : nl_fo_formula_list int int ;
      nlfree_var_symbol_set_abstraction_fo_formula_list_field : int ;
      nlfree_var_fo_term_set_abstraction_fo_formula_list_field : int ;
      ghost model_fo_formula_list_field : fo_formula_list int int ;
    }

  type cons_fo_formula_list = | NLC_FOFNil
    | NLC_FOFCons (nlimpl_fo_formula) (nlimpl_fo_formula_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 Firstorder_formula_impl.Types
  use Firstorder_formula_impl.Logic
  use Firstorder_formula_impl.Impl
  use Firstorder_formula_list_spec.Spec
  use Types
  function nat_nlsize_fo_formula_list (t:nl_fo_formula_list 'b0 'b1) : nat =
    match t with | NL_FOFNil -> let s = one_nat in s
      | NL_FOFCons v0 v1 ->
        let s = one_nat in
          let s = add_nat (nat_nlsize_fo_formula_list v1) s in
          let s = add_nat (nat_nlsize_fo_formula v0) s in s
    end

  with nlsize_fo_formula_list (t:nl_fo_formula_list 'b0 'b1) : int =
    match t with | NL_FOFNil -> let s = 1 in s
      | NL_FOFCons v0 v1 ->
        let s = 1 in let s = nlsize_fo_formula_list v1 + s in
          let s = nlsize_fo_formula v0 + s in s
    end

  let rec lemma nlsize_positive_lemma_fo_formula_list
    (t:nl_fo_formula_list 'b0 'b1) : unit
    ensures { nlsize_fo_formula_list t > 0 }
    variant { nat_to_int (nat_nlsize_fo_formula_list t) } =
    match t with | NL_FOFNil -> ()
      | NL_FOFCons v0 v1 ->
        nlsize_positive_lemma_fo_formula v0 ;
          nlsize_positive_lemma_fo_formula_list v1 ; ()
    end

  function nlmodel_fo_formula_list (t:nl_fo_formula_list 'b0 'b1)
    (fr0:'b0 -> (symbol 'c0)) (bnd0: int -> (symbol 'c0))
    (fr1:'b1 -> (fo_term 'c0 'c1)) (bnd1: int -> (fo_term 'c0 'c1)) :
    fo_formula_list 'c0 'c1 =
    match t with | NL_FOFNil -> FOFNil
      | NL_FOFCons v0 v1 ->
        FOFCons
          (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_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_list
    (t:nl_fo_formula_list '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_list 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_list (nlmodel_fo_formula_list t fr0 bnd0 fr1 bnd1) s0
        s1
      }
    variant { nlsize_fo_formula_list t } =
    match t with | NL_FOFNil -> ()
      | NL_FOFCons 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_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_list
    (t:nl_fo_formula_list '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_list 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_list (nlmodel_fo_formula_list t fr0 bnd0 fr1 bnd1) s0
        s1
      }
    =
    nlmodel_subst_commutation_lemma_fo_formula_list t fr0 bnd0
      (subst_of_rename_symbol s0) fr1 bnd1 (subst_of_rename_fo_term s1)

  predicate correct_indexes_fo_formula_list (t:nl_fo_formula_list 'b0 'b1) =
    match t with | NL_FOFNil -> true
      | NL_FOFCons v0 v1 ->
        correct_indexes_fo_formula v0 /\ correct_indexes_fo_formula_list v1
    end

  function bound_depth_of_symbol_in_fo_formula_list
    (t:nl_fo_formula_list 'b0 'b1) : int =
    match t with | NL_FOFNil -> 0
      | NL_FOFCons 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_list v1 in
          let a = if a > b then a else b in a
    end

  with bound_depth_of_fo_term_in_fo_formula_list
    (t:nl_fo_formula_list 'b0 'b1) : int =
    match t with | NL_FOFNil -> 0
      | NL_FOFCons 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_list v1 in
          let a = if a > b then a else b in a
    end

  let rec lemma bound_depth_of_symbol_in_fo_formula_list_nonnegative
    (t:nl_fo_formula_list 'b0 'b1) : unit
    requires { correct_indexes_fo_formula_list t }
    ensures { bound_depth_of_symbol_in_fo_formula_list t >= 0 }
    variant { nlsize_fo_formula_list t } =
    match t with | NL_FOFNil -> ()
      | NL_FOFCons v0 v1 ->
        bound_depth_of_symbol_in_fo_formula_nonnegative v0 ;
          bound_depth_of_symbol_in_fo_formula_list_nonnegative v1 ; ()
    end

  with lemma bound_depth_of_fo_term_in_fo_formula_list_nonnegative
    (t:nl_fo_formula_list 'b0 'b1) : unit
    requires { correct_indexes_fo_formula_list t }
    ensures { bound_depth_of_fo_term_in_fo_formula_list t >= 0 }
    variant { nlsize_fo_formula_list t } =
    match t with | NL_FOFNil -> ()
      | NL_FOFCons v0 v1 ->
        bound_depth_of_fo_term_in_fo_formula_nonnegative v0 ;
          bound_depth_of_fo_term_in_fo_formula_list_nonnegative v1 ; ()
    end

  let rec lemma model_equal_fo_formula_list (t:nl_fo_formula_list '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_list t ->
        bnd10 i = bnd20 i
      }
    requires { fr10 = fr20 }
    requires {
      forall i:int. 0 <= i < bound_depth_of_fo_term_in_fo_formula_list t ->
        bnd11 i = bnd21 i
      }
    requires { fr11 = fr21 } requires { correct_indexes_fo_formula_list t }
    ensures { nlmodel_fo_formula_list t fr10 bnd10 fr11 bnd11 =
      nlmodel_fo_formula_list t fr20 bnd20 fr21 bnd21 }
    variant { nlsize_fo_formula_list t } =
    match t with | NL_FOFNil -> ()
      | NL_FOFCons 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_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_list_ok (t:nlimpl_fo_formula_list) =
    nlmodel_fo_formula_list t.nlrepr_fo_formula_list_field subst_id_symbol
      (const (Var_symbol ((-1)))) subst_id_fo_term
      (const (Var_fo_term ((-1)))) = t.model_fo_formula_list_field
    /\ correct_indexes_fo_formula_list t.nlrepr_fo_formula_list_field /\
    bound_depth_of_symbol_in_fo_formula_list t.nlrepr_fo_formula_list_field =
      0
    /\
    bound_depth_of_fo_term_in_fo_formula_list t.nlrepr_fo_formula_list_field
      = 0
    /\
    (forall x:int.
       is_symbol_free_var_in_fo_formula_list x t.model_fo_formula_list_field
       -> (x) < (t.nlfree_var_symbol_set_abstraction_fo_formula_list_field))
    /\
    (forall x:int.
       is_fo_term_free_var_in_fo_formula_list x t.model_fo_formula_list_field
       -> (x) < (t.nlfree_var_fo_term_set_abstraction_fo_formula_list_field))

  predicate cons_ok_fo_formula_list (c:cons_fo_formula_list) =
    match c with | NLC_FOFNil -> true
      | NLC_FOFCons v0 v1 -> nlimpl_fo_formula_ok v0 /\
        nlimpl_fo_formula_list_ok v1
    end

  predicate cons_rel_fo_formula_list (c:cons_fo_formula_list)
    (t:nlimpl_fo_formula_list) =
    match c with | NLC_FOFNil -> t.model_fo_formula_list_field = FOFNil
      | NLC_FOFCons v0 v1 -> t.model_fo_formula_list_field =
        FOFCons
          (rename_fo_formula v0.model_fo_formula_field identity identity)
          (rename_fo_formula_list v1.model_fo_formula_list_field identity
             identity)
    end

  predicate cons_open_rel_fo_formula_list (c:cons_fo_formula_list)
    (t:nlimpl_fo_formula_list) =
    match c with
      | NLC_FOFNil ->
        match t.model_fo_formula_list_field with | FOFNil -> true
          | FOFCons w0 w1 -> false
        end
      | NLC_FOFCons v0 v1 ->
        match t.model_fo_formula_list_field with | FOFNil -> false
          | FOFCons w0 w1 ->
            v0.model_fo_formula_field =
              (rename_fo_formula w0 identity identity) /\
              v1.model_fo_formula_list_field =
                (rename_fo_formula_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 Firstorder_formula_impl.Types
  use Firstorder_formula_impl.Logic
  use Firstorder_formula_impl.Impl
  use Firstorder_formula_list_spec.Spec
  use Types
  use Logic
  let rec bind_var_symbol_in_fo_formula_list (t:nl_fo_formula_list 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_list int int
    requires { correct_indexes_fo_formula_list t }
    requires { bound_depth_of_symbol_in_fo_formula_list t <= i }
    variant { nlsize_fo_formula_list t }
    ensures { bound_depth_of_symbol_in_fo_formula_list result <= i + 1 }
    ensures { correct_indexes_fo_formula_list result }
    ensures { bound_depth_of_fo_term_in_fo_formula_list t =
      bound_depth_of_fo_term_in_fo_formula_list result }
    ensures { nlmodel_fo_formula_list result fr0 bnd0 fr1 bnd1 =
      nlmodel_fo_formula_list t (update fr0 x (bnd0 i)) bnd0 fr1 bnd1 }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (t:nl_fo_formula_list 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_list int int
    requires { correct_indexes_fo_formula_list t }
    requires { bound_depth_of_fo_term_in_fo_formula_list t <= i }
    variant { nlsize_fo_formula_list t }
    ensures { bound_depth_of_fo_term_in_fo_formula_list result <= i + 1 }
    ensures { correct_indexes_fo_formula_list result }
    ensures { bound_depth_of_symbol_in_fo_formula_list t =
      bound_depth_of_symbol_in_fo_formula_list result }
    ensures { nlmodel_fo_formula_list result fr0 bnd0 fr1 bnd1 =
      nlmodel_fo_formula_list t fr0 bnd0 (update fr1 x (bnd1 i)) bnd1 }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (t:nl_fo_formula_list 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_list int int
    requires { i >= 0 } requires { correct_indexes_fo_formula_list t }
    requires { bound_depth_of_symbol_in_fo_formula_list t <= i + 1 }
    requires { correct_indexes_symbol x }
    requires { bound_depth_of_symbol_in_symbol x = 0 }
    variant { nlsize_fo_formula_list t }
    ensures { correct_indexes_fo_formula_list result }
    ensures { bound_depth_of_symbol_in_fo_formula_list result <= i }
    ensures { bound_depth_of_fo_term_in_fo_formula_list result =
      bound_depth_of_fo_term_in_fo_formula_list t }
    ensures { nlmodel_fo_formula_list result fr0 bnd10 fr1 bnd11 =
      nlmodel_fo_formula_list t fr0
        (update bnd10 i (nlmodel_symbol x fr0 bnd20)) fr1 bnd11
      }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (t:nl_fo_formula_list 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_list int int
    requires { i >= 0 } requires { correct_indexes_fo_formula_list t }
    requires { bound_depth_of_fo_term_in_fo_formula_list t <= i + 1 }
    requires { correct_indexes_fo_term x }
    requires { bound_depth_of_symbol_in_fo_term x = 0 }
    requires { bound_depth_of_fo_term_in_fo_term x = 0 }
    variant { nlsize_fo_formula_list t }
    ensures { correct_indexes_fo_formula_list result }
    ensures { bound_depth_of_fo_term_in_fo_formula_list result <= i }
    ensures { bound_depth_of_symbol_in_fo_formula_list result =
      bound_depth_of_symbol_in_fo_formula_list t }
    ensures { nlmodel_fo_formula_list result fr0 bnd10 fr1 bnd11 =
      nlmodel_fo_formula_list t fr0 bnd10 fr1
        (update bnd11 i (nlmodel_fo_term x fr0 bnd20 fr1 bnd21))
      }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (t:nl_fo_formula_list 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_list int int
    requires { correct_indexes_fo_formula_list t }
    requires { correct_indexes_symbol u }
    requires { bound_depth_of_symbol_in_symbol u = 0 }
    variant { nlsize_fo_formula_list t }
    ensures { correct_indexes_fo_formula_list result }
     ensures { bound_depth_of_symbol_in_fo_formula_list result =
       bound_depth_of_symbol_in_fo_formula_list t }
    ensures { bound_depth_of_fo_term_in_fo_formula_list result =
      bound_depth_of_fo_term_in_fo_formula_list t }
    ensures { nlmodel_fo_formula_list result fr0 bnd10 fr1 bnd11 =
      nlmodel_fo_formula_list t (update fr0 x (nlmodel_symbol u fr0 bnd20))
        bnd10 fr1 bnd11
      }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (t:nl_fo_formula_list 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_list int int
    requires { correct_indexes_fo_formula_list t }
    requires { correct_indexes_fo_term u }
    requires { bound_depth_of_symbol_in_fo_term u = 0 }
    requires { bound_depth_of_fo_term_in_fo_term u = 0 }
    variant { nlsize_fo_formula_list t }
    ensures { correct_indexes_fo_formula_list result }
     ensures { bound_depth_of_symbol_in_fo_formula_list result =
       bound_depth_of_symbol_in_fo_formula_list t }
    ensures { bound_depth_of_fo_term_in_fo_formula_list result =
      bound_depth_of_fo_term_in_fo_formula_list t }
    ensures { nlmodel_fo_formula_list result fr0 bnd10 fr1 bnd11 =
      nlmodel_fo_formula_list t fr0 bnd10
        (update fr1 x (nlmodel_fo_term u fr0 bnd20 fr1 bnd21)) bnd11
      }
    =
    match t with | NL_FOFNil -> NL_FOFNil
      | NL_FOFCons 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_FOFCons
            (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_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_list (c:cons_fo_formula_list) :
    nlimpl_fo_formula_list requires { cons_ok_fo_formula_list c }
    ensures { nlimpl_fo_formula_list_ok result }
    ensures { cons_rel_fo_formula_list c result }
    (*ensures { cons_open_rel_fo_formula_list c result }*) =
    match c with
      | NLC_FOFNil ->
        let res =
          { nlrepr_fo_formula_list_field = (NL_FOFNil) ;
            nlfree_var_symbol_set_abstraction_fo_formula_list_field = 0 ;
            nlfree_var_fo_term_set_abstraction_fo_formula_list_field = 0 ;
            model_fo_formula_list_field = ghost (FOFNil) ;
          }
        in
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_formula_list x
              res.model_fo_formula_list_field
            -> (false) && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_formula_list x
              res.model_fo_formula_list_field
            -> (false) && (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
          } ;
        res
      | NLC_FOFCons v0 v1 -> assert { nlimpl_fo_formula_ok v0 } ;
        assert { nlimpl_fo_formula_list_ok v1 } ;
        let res =
          {
            nlrepr_fo_formula_list_field =
              (NL_FOFCons (let v0 = v0.nlrepr_fo_formula_field in v0)
                 (let v1 = v1.nlrepr_fo_formula_list_field in v1)) ;
            nlfree_var_symbol_set_abstraction_fo_formula_list_field =
              (let aux (a:int) (b:int) : int
                 ensures { result >= a /\ result >= b } =
                 if a < b then b else a in
                 aux (v0.nlfree_var_symbol_set_abstraction_fo_formula_field)
                   (v1.nlfree_var_symbol_set_abstraction_fo_formula_list_field)) ;
            nlfree_var_fo_term_set_abstraction_fo_formula_list_field =
              (let aux (a:int) (b:int) : int
                 ensures { result >= a /\ result >= b } =
                 if a < b then b else a in
                 aux (v0.nlfree_var_fo_term_set_abstraction_fo_formula_field)
                   (v1.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)) ;
            model_fo_formula_list_field = ghost
              (FOFCons
                 (rename_fo_formula v0.model_fo_formula_field identity
                    identity)
                 (rename_fo_formula_list v1.model_fo_formula_list_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_list_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_list_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_formula_list x
              (rename_fo_formula_list v1.model_fo_formula_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_symbol_free_var_in_fo_formula_list y
                  v1.model_fo_formula_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_symbol_free_var_in_fo_formula_list x
                 v1.model_fo_formula_list_field)
            &&
            is_symbol_free_var_in_fo_formula_list x
              v1.model_fo_formula_list_field
            && (x) <
            (v1.nlfree_var_symbol_set_abstraction_fo_formula_list_field) &&
            (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_formula_list x
              (rename_fo_formula_list v1.model_fo_formula_list_field identity
                 identity)
            ->
            (forall y:int.
               (is_fo_term_free_var_in_fo_formula_list y
                  v1.model_fo_formula_list_field
               /\ eval (identity) y = x) -> x = eval (identity) y &&
               x = y &&
               is_fo_term_free_var_in_fo_formula_list x
                 v1.model_fo_formula_list_field)
            &&
            is_fo_term_free_var_in_fo_formula_list x
              v1.model_fo_formula_list_field
            && (x) <
            (v1.nlfree_var_fo_term_set_abstraction_fo_formula_list_field) &&
            (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
          } ;
        assert {
          forall x:int.
            is_symbol_free_var_in_fo_formula_list x
              res.model_fo_formula_list_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_list x
                 (rename_fo_formula_list v1.model_fo_formula_list_field
                    identity identity))
            && (x) <
            (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
          } ;
        assert {
          forall x:int.
            is_fo_term_free_var_in_fo_formula_list x
              res.model_fo_formula_list_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_list x
                 (rename_fo_formula_list v1.model_fo_formula_list_field
                    identity identity))
            && (x) <
            (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
          } ;
        assert {
          extensionalEqual (rename_subst_symbol subst_id_symbol identity)
            ((rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
                identity))
          } ;
        assert { rename_subst_symbol subst_id_symbol identity =
          (rename_subst_symbol (subst_id_symbol:(int)->(symbol (int)))
             identity)
          } ;
        assert {
          extensionalEqual
            (rename_subst_fo_term subst_id_fo_term identity identity)
            ((rename_subst_fo_term
                (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
                identity))
          } ;
        assert { rename_subst_fo_term subst_id_fo_term identity identity =
          (rename_subst_fo_term
             (subst_id_fo_term:(int)->(fo_term (int) (int))) identity
             identity)
          } ;
        model_equal_fo_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_list v1.nlrepr_fo_formula_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_list (t:nlimpl_fo_formula_list) :
    cons_fo_formula_list requires { nlimpl_fo_formula_list_ok t }
    ensures { cons_ok_fo_formula_list result }
    ensures { cons_rel_fo_formula_list result t }
    ensures { cons_open_rel_fo_formula_list result t } =
    let fv0 = t.nlfree_var_symbol_set_abstraction_fo_formula_list_field in
    let fv1 = t.nlfree_var_fo_term_set_abstraction_fo_formula_list_field in
    match t.nlrepr_fo_formula_list_field with
      | NL_FOFNil ->
        assert { t.model_fo_formula_list_field = FOFNil } ;
          let () =
            match t.model_fo_formula_list_field with | FOFNil -> ()
              | FOFCons x0 x1 -> absurd
            end
          in let res = NLC_FOFNil in res
      | NL_FOFCons v0 v1 ->
        assert { t.model_fo_formula_list_field =
          FOFCons
            (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_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_list_field with | FOFNil -> absurd
              | FOFCons x0 x1 -> (x0 , x1)
            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_list v1
              ((rename_subst_symbol subst_id_symbol identity))
              ((rename_subst_symbol
                 (const (Var_symbol (-1)) : int -> (symbol int)) identity))
              ((rename_subst_fo_term subst_id_fo_term identity identity))
              ((rename_subst_fo_term
                 (const (Var_fo_term (-1)) : int -> (fo_term int int))
                 identity identity))
            } ;
          assert { bound_depth_of_symbol_in_fo_formula v0 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_formula x mv0 ->
              is_symbol_free_var_in_fo_formula_list x
                t.model_fo_formula_list_field
              && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_formula_list_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_list x
                t.model_fo_formula_list_field
              && (x) <
              (t.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
            } ;
          assert { bound_depth_of_symbol_in_fo_formula_list v1 <= 0 } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_formula_list x mv1 ->
              is_symbol_free_var_in_fo_formula_list x
                t.model_fo_formula_list_field
              && (x) <
              (t.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
            } ;
          assert { bound_depth_of_fo_term_in_fo_formula_list v1 <= 0 } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_formula_list x mv1 ->
              is_fo_term_free_var_in_fo_formula_list x
                t.model_fo_formula_list_field
              && (x) <
              (t.nlfree_var_fo_term_set_abstraction_fo_formula_list_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_list v1 subst_id_symbol
            (rename_subst_symbol
               ((rename_subst_symbol subst_id_symbol identity)) (identity)) ((
            const (Var_symbol (-1)) : int -> (symbol int)))
            (rename_subst_symbol
               ((rename_subst_symbol
                  (const (Var_symbol (-1)) : int -> (symbol int)) identity))
               (identity))
            subst_id_fo_term
            (rename_subst_fo_term
               ((rename_subst_fo_term subst_id_fo_term identity identity))
               (identity) (identity)) ((const (Var_fo_term (-1)) :
                                          int -> (fo_term int int)))
            (rename_subst_fo_term
               ((rename_subst_fo_term
                  (const (Var_fo_term (-1)) : int -> (fo_term int int))
                  identity identity))
               (identity) (identity)) ;
          let ghost mrv0 = rename_fo_formula mv0 identity identity in
          let ghost mrv1 = rename_fo_formula_list 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_list_field = v1 ;
              nlfree_var_symbol_set_abstraction_fo_formula_list_field = fv0 ;
              nlfree_var_fo_term_set_abstraction_fo_formula_list_field =
                fv1 ;
              model_fo_formula_list_field = ghost mrv1 ;
            }
          in let res = NLC_FOFCons 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_list 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_list x
                   t.model_fo_formula_list_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_list x
                   t.model_fo_formula_list_field
                 && (x) < (fv1))
              && (x) < (fv1)
            } ;
          assert {
            forall x:int. is_symbol_free_var_in_fo_formula_list x mrv1 ->
              (forall y:int.
                 (is_symbol_free_var_in_fo_formula_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_symbol_free_var_in_fo_formula_list x
                   t.model_fo_formula_list_field
                 && (x) < (fv0))
              && (x) < (fv0)
            } ;
          assert {
            forall x:int. is_fo_term_free_var_in_fo_formula_list x mrv1 ->
              (forall y:int.
                 (is_fo_term_free_var_in_fo_formula_list y mv1 /\
                    eval (identity) y = x)
                 -> x = y &&
                 is_fo_term_free_var_in_fo_formula_list x
                   t.model_fo_formula_list_field
                 && (x) < (fv1))
              && (x) < (fv1)
            } ;
          res
    end

  let nlsubst_symbol_in_fo_formula_list (t:nlimpl_fo_formula_list) (x:int)
    (u:nlimpl_symbol) : nlimpl_fo_formula_list
    requires { nlimpl_fo_formula_list_ok t } requires { nlimpl_symbol_ok u }
    ensures { nlimpl_fo_formula_list_ok result }
    ensures { result.model_fo_formula_list_field =
      subst_fo_formula_list t.model_fo_formula_list_field
        (update (subst_id_symbol: (int) -> (symbol (int))) x
           u.model_symbol_field)
        (subst_id_fo_term: (int) -> (fo_term (int) (int)))
      }
    =
    model_equal_fo_formula_list t.nlrepr_fo_formula_list_field
      (subst_compose_symbol subst_id_symbol
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((update (subst_id_symbol: (int) -> (symbol (int))) x
          u.model_symbol_field))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field)))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((update (subst_id_symbol: (int) -> (symbol (int))) x
             u.model_symbol_field))
         ((subst_id_fo_term: (int) -> (fo_term (int) (int)))))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_formula_list_field =
          subst_base_symbol_in_fo_formula_list t.nlrepr_fo_formula_list_field
            x u.nlrepr_symbol_field (subst_id_symbol)
            ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_formula_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
               (u.nlfree_var_symbol_set_abstraction_symbol_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_formula_list_field =
          t.nlfree_var_fo_term_set_abstraction_fo_formula_list_field ;
        model_fo_formula_list_field = ghost
          subst_fo_formula_list t.model_fo_formula_list_field
            (update (subst_id_symbol: (int) -> (symbol (int))) x
               u.model_symbol_field)
            (subst_id_fo_term: (int) -> (fo_term (int) (int))) ;
      }
    in
    assert {
      forall x2:int.
        is_symbol_free_var_in_fo_formula_list x2
          res.model_fo_formula_list_field
        ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval
                      ((update (subst_id_symbol: (int) -> (symbol (int))) x
                          u.model_symbol_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)))
                 && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> false))
        && (x2) <
        (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_formula_list x2
          res.model_fo_formula_list_field
        ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval ((subst_id_fo_term: (int) -> (fo_term (int) (int))))
                      y))
              -> x2 = y && (x2) <
              (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)))
        && (x2) <
        (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
      } ;
    res

  let nlsubst_fo_term_in_fo_formula_list (t:nlimpl_fo_formula_list) (x:int)
    (u:nlimpl_fo_term) : nlimpl_fo_formula_list
    requires { nlimpl_fo_formula_list_ok t } requires { nlimpl_fo_term_ok u }
    ensures { nlimpl_fo_formula_list_ok result }
    ensures { result.model_fo_formula_list_field =
      subst_fo_formula_list t.model_fo_formula_list_field
        (subst_id_symbol: (int) -> (symbol (int)))
        (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
           u.model_fo_term_field)
      }
    =
    model_equal_fo_formula_list t.nlrepr_fo_formula_list_field
      (subst_compose_symbol subst_id_symbol
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((subst_id_symbol: (int) -> (symbol (int))))
      (subst_compose_symbol (const (Var_symbol (-1)))
         ((subst_id_symbol: (int) -> (symbol (int)))))
      ((const (Var_symbol (-1))))
      (subst_compose_fo_term subst_id_fo_term
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
          u.model_fo_term_field))
      (subst_compose_fo_term (const (Var_fo_term (-1)))
         ((subst_id_symbol: (int) -> (symbol (int))))
         ((update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
             u.model_fo_term_field)))
      ((const (Var_fo_term (-1))));
    let res =
      {
        nlrepr_fo_formula_list_field =
          subst_base_fo_term_in_fo_formula_list
            t.nlrepr_fo_formula_list_field x u.nlrepr_fo_term_field
            (subst_id_symbol) ((const (Var_symbol (-1)))) (subst_id_fo_term)
            ((const (Var_fo_term (-1)))) ((const (Var_symbol (-1))))
            ((const (Var_fo_term (-1)))) ;
        nlfree_var_symbol_set_abstraction_fo_formula_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
               (u.nlfree_var_symbol_set_abstraction_fo_term_field)) ;
        nlfree_var_fo_term_set_abstraction_fo_formula_list_field =
          (let aux (a:int) (b:int) : int
             ensures { result >= a /\ result >= b } = if a < b then b else a
             in
             aux (t.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
               (u.nlfree_var_fo_term_set_abstraction_fo_term_field)) ;
        model_fo_formula_list_field = ghost
          subst_fo_formula_list t.model_fo_formula_list_field
            (subst_id_symbol: (int) -> (symbol (int)))
            (update (subst_id_fo_term: (int) -> (fo_term (int) (int))) x
               u.model_fo_term_field) ;
      }
    in
    assert {
      forall x2:int.
        is_symbol_free_var_in_fo_formula_list x2
          res.model_fo_formula_list_field
        ->
        (true /\
           (forall y:int.
              (is_symbol_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_symbol_free_var_in_symbol x2
                   (eval ((subst_id_symbol: (int) -> (symbol (int)))) y))
              -> x2 = y && (x2) <
              (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field))
           /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_symbol_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field))
                 /\ (x <> y -> false)) && (x2) <
                 (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)))
        && (x2) <
        (res.nlfree_var_symbol_set_abstraction_fo_formula_list_field)
      } ;
    assert {
      forall x2:int.
        is_fo_term_free_var_in_fo_formula_list x2
          res.model_fo_formula_list_field
        ->
        (true /\
           (forall y:int.
              (is_fo_term_free_var_in_fo_formula_list y
                 t.model_fo_formula_list_field /\
                 is_fo_term_free_var_in_fo_term x2
                   (eval
                      ((update
                          (subst_id_fo_term: (int) -> (fo_term (int) (int)))
                          x u.model_fo_term_field))
                      y))
              ->
              ((x = y -> (x2) <
                  (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field))
                 /\
                 (x <> y -> x2 = y && (x2) <
                    (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)))
                 && (x2) <
                 (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)))
        && (x2) <
        (res.nlfree_var_fo_term_set_abstraction_fo_formula_list_field)
      } ;
    res

end