# Theory Satisfies_absolute

Up to index of Isabelle/ZF/Constructible

theory Satisfies_absolute
imports Datatype_absolute Rec_Separation
begin

    (*  Title:      ZF/Constructible/Satisfies_absolute.thy
        ID:  $Id: Satisfies_absolute.thy,v 1.15 2005/06/17 14:15:10 haftmann Exp $
        Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    *)

    header {*Absoluteness for the Satisfies Relation on Formulas*}

    theory Satisfies_absolute imports Datatype_absolute Rec_Separation begin

    subsection {*More Internalization*}

    subsubsection{*The Formula @{term is_depth}, Internalized*}

    (*    "is_depth(M,p,n) ==
           ∃sn[M]. ∃formula_n[M]. ∃formula_sn[M].
             2          1                0
            is_formula_N(M,n,formula_n) & p ∉ formula_n &
            successor(M,n,sn) & is_formula_N(M,sn,formula_sn) & p ∈ formula_sn" *)
    constdefs depth_fm :: "[i,i]=>i"
      "depth_fm(p,n) ==
         Exists(Exists(Exists(
           And(formula_N_fm(n#+3,1),
             And(Neg(Member(p#+3,1)),
              And(succ_fm(n#+3,2),
               And(formula_N_fm(2,0), Member(p#+3,0))))))))"

    lemma depth_fm_type [TC]:
     "[| x ∈ nat; y ∈ nat |] ==> depth_fm(x,y) ∈ formula"
    by (simp add: depth_fm_def)

    lemma sats_depth_fm [simp]:
       "[| x ∈ nat; y < length(env); env ∈ list(A)|]
        ==> sats(A, depth_fm(x,y), env) <->
            is_depth(##A, nth(x,env), nth(y,env))"
    apply (frule_tac x=y in lt_length_in_nat, assumption)
    apply (simp add: depth_fm_def is_depth_def)
    done

    lemma depth_iff_sats:
          "[| nth(i,env) = x; nth(j,env) = y;
              i ∈ nat; j < length(env); env ∈ list(A)|]
           ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i,j), env)"
    by (simp add: sats_depth_fm)

    theorem depth_reflection:
         "REFLECTS[λx. is_depth(L, f(x), g(x)),
                   λi x. is_depth(##Lset(i), f(x), g(x))]"
    apply (simp only: is_depth_def)
    apply (intro FOL_reflections function_reflections formula_N_reflection)
    done

    subsubsection{*The Operator @{term is_formula_case}*}

    text{*The arguments of @{term is_a} are always 2, 1, 0, and the formula
          will be enclosed by three quantifiers.*}

    (* is_formula_case ::
        "[i=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i,i]=>o, [i,i]=>o, i, i] => o"
      "is_formula_case(M, is_a, is_b, is_c, is_d, v, z) ==
          (∀x[M]. ∀y[M]. x∈nat --> y∈nat --> is_Member(M,x,y,v) --> is_a(x,y,z)) &
          (∀x[M]. ∀y[M]. x∈nat --> y∈nat --> is_Equal(M,x,y,v) --> is_b(x,y,z)) &
          (∀x[M]. ∀y[M]. x∈formula --> y∈formula -->
                         is_Nand(M,x,y,v) --> is_c(x,y,z)) &
          (∀x[M]. x∈formula --> is_Forall(M,x,v) --> is_d(x,z))" *)

    constdefs formula_case_fm :: "[i, i, i, i, i, i]=>i"
     "formula_case_fm(is_a, is_b, is_c, is_d, v, z) ==
            And(Forall(Forall(Implies(finite_ordinal_fm(1),
                               Implies(finite_ordinal_fm(0),
                                Implies(Member_fm(1,0,v#+2),
                                 Forall(Implies(Equal(0,z#+3), is_a))))))),
            And(Forall(Forall(Implies(finite_ordinal_fm(1),
                               Implies(finite_ordinal_fm(0),
                                Implies(Equal_fm(1,0,v#+2),
                                 Forall(Implies(Equal(0,z#+3), is_b))))))),
            And(Forall(Forall(Implies(mem_formula_fm(1),
                               Implies(mem_formula_fm(0),
                                Implies(Nand_fm(1,0,v#+2),
                                 Forall(Implies(Equal(0,z#+3), is_c))))))),
            Forall(Implies(mem_formula_fm(0),
                           Implies(Forall_fm(0,succ(v)),
                                 Forall(Implies(Equal(0,z#+2), is_d))))))))"

    lemma is_formula_case_type [TC]:
         "[| is_a ∈ formula;  is_b ∈ formula;  is_c ∈ formula;  is_d ∈ formula;
             x ∈ nat; y ∈ nat |]
          ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) ∈ formula"
    by (simp add: formula_case_fm_def)

    lemma sats_formula_case_fm:
      assumes is_a_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_b_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_c_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_d_iff_sats:
          "!!a0 a1.
            [|a0∈A; a1∈A|]
            ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
      shows
          "[|x ∈ nat; y < length(env); env ∈ list(A)|]
           ==> sats(A, formula_case_fm(is_a,is_b,is_c,is_d,x,y), env) <->
               is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x,env), nth(y,env))"
    apply (frule_tac x=y in lt_length_in_nat, assumption)
    apply (simp add: formula_case_fm_def is_formula_case_def
                     is_a_iff_sats [THEN iff_sym] is_b_iff_sats [THEN iff_sym]
                     is_c_iff_sats [THEN iff_sym] is_d_iff_sats [THEN iff_sym])
    done

    lemma formula_case_iff_sats:
      assumes is_a_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_b_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_c_iff_sats:
          "!!a0 a1 a2.
            [|a0∈A; a1∈A; a2∈A|]
            ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0,Cons(a1,Cons(a2,env))))"
      and is_d_iff_sats:
          "!!a0 a1.
            [|a0∈A; a1∈A|]
            ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0,Cons(a1,env)))"
      shows
          "[|nth(i,env) = x; nth(j,env) = y;
          i ∈ nat; j < length(env); env ∈ list(A)|]
           ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
               sats(A, formula_case_fm(is_a,is_b,is_c,is_d,i,j), env)"
    by (simp add: sats_formula_case_fm [OF is_a_iff_sats is_b_iff_sats
                                           is_c_iff_sats is_d_iff_sats])

    text{*The second argument of @{term is_a} gives it direct access to @{term x},
      which is essential for handling free variable references.  Treatment is
      based on that of @{text is_nat_case_reflection}.*}
    theorem is_formula_case_reflection:
      assumes is_a_reflection:
        "!!h f g g'. REFLECTS[λx. is_a(L, h(x), f(x), g(x), g'(x)),
                         λi x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))]"
      and is_b_reflection:
        "!!h f g g'. REFLECTS[λx. is_b(L, h(x), f(x), g(x), g'(x)),
                         λi x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))]"
      and is_c_reflection:
        "!!h f g g'. REFLECTS[λx. is_c(L, h(x), f(x), g(x), g'(x)),
                         λi x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))]"
      and is_d_reflection:
        "!!h f g g'. REFLECTS[λx. is_d(L, h(x), f(x), g(x)),
                         λi x. is_d(##Lset(i), h(x), f(x), g(x))]"
      shows "REFLECTS[λx. is_formula_case(L, is_a(L,x), is_b(L,x), is_c(L,x), is_d(L,x), g(x), h(x)),
                   λi x. is_formula_case(##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x), is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]"
    apply (simp (no_asm_use) only: is_formula_case_def)
    apply (intro FOL_reflections function_reflections finite_ordinal_reflection
             mem_formula_reflection
             Member_reflection Equal_reflection Nand_reflection Forall_reflection
             is_a_reflection is_b_reflection is_c_reflection is_d_reflection)
    done

    subsection {*Absoluteness for the Function @{term satisfies}*}

    constdefs
      is_depth_apply :: "[i=>o,i,i,i] => o"
       --{*Merely a useful abbreviation for the sequel.*}
       "is_depth_apply(M,h,p,z) ==
        ∃dp[M]. ∃sdp[M]. ∃hsdp[M].
            finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
            fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z)"

    lemma (in M_datatypes) is_depth_apply_abs [simp]:
         "[|M(h); p ∈ formula; M(z)|]
          ==> is_depth_apply(M,h,p,z) <-> z = h ` succ(depth(p)) ` p"
    by (simp add: is_depth_apply_def formula_into_M depth_type eq_commute)

    text{*There is at present some redundancy between the relativizations in
     e.g. @{text satisfies_is_a} and those in e.g. @{text Member_replacement}.*}

    text{*These constants let us instantiate the parameters @{term a}, @{term b},
          @{term c}, @{term d}, etc., of the locale @{text Formula_Rec}.*}
    constdefs
      satisfies_a :: "[i,i,i]=>i"
       "satisfies_a(A) ==
        λx y. λenv ∈ list(A). bool_of_o (nth(x,env) ∈ nth(y,env))"

      satisfies_is_a :: "[i=>o,i,i,i,i]=>o"
       "satisfies_is_a(M,A) ==
        λx y zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. is_bool_of_o(M,
                          ∃nx[M]. ∃ny[M].
                           is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx ∈ ny, z),
                    zz)"

      satisfies_b :: "[i,i,i]=>i"
       "satisfies_b(A) ==
        λx y. λenv ∈ list(A). bool_of_o (nth(x,env) = nth(y,env))"

      satisfies_is_b :: "[i=>o,i,i,i,i]=>o"
       --{*We simplify the formula to have just @{term nx} rather than
           introducing @{term ny} with  @{term "nx=ny"} *}
       "satisfies_is_b(M,A) ==
        λx y zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. is_bool_of_o(M,
                          ∃nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
                    zz)"

      satisfies_c :: "[i,i,i,i,i]=>i"
       "satisfies_c(A) == λp q rp rq. λenv ∈ list(A). not(rp ` env and rq ` env)"

      satisfies_is_c :: "[i=>o,i,i,i,i,i]=>o"
       "satisfies_is_c(M,A,h) ==
        λp q zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA, λenv z. ∃hp[M]. ∃hq[M].
                     (∃rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) &
                     (∃rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) &
                     (∃pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
                    zz)"

      satisfies_d :: "[i,i,i]=>i"
       "satisfies_d(A)
        == λp rp. λenv ∈ list(A). bool_of_o (∀x∈A. rp ` (Cons(x,env)) = 1)"

      satisfies_is_d :: "[i=>o,i,i,i,i]=>o"
       "satisfies_is_d(M,A,h) ==
        λp zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. ∃rp[M]. is_depth_apply(M,h,p,rp) &
                        is_bool_of_o(M,
                               ∀x[M]. ∀xenv[M]. ∀hp[M].
                                  x∈A --> is_Cons(M,x,env,xenv) -->
                                  fun_apply(M,rp,xenv,hp) --> number1(M,hp),
                      z),
                   zz)"

      satisfies_MH :: "[i=>o,i,i,i,i]=>o"
        --{*The variable @{term u} is unused, but gives @{term satisfies_MH}
            the correct arity.*}
       "satisfies_MH ==
        λM A u f z.
             ∀fml[M]. is_formula(M,fml) -->
                 is_lambda (M, fml,
                   is_formula_case (M, satisfies_is_a(M,A),
                                    satisfies_is_b(M,A),
                                    satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
                   z)"

      is_satisfies :: "[i=>o,i,i,i]=>o"
       "is_satisfies(M,A) == is_formula_rec (M, satisfies_MH(M,A))"

    text{*This lemma relates the fragments defined above to the original primitive
          recursion in @{term satisfies}.
          Induction is not required: the definitions are directly equal!*}
    lemma satisfies_eq:
      "satisfies(A,p) =
       formula_rec (satisfies_a(A), satisfies_b(A),
                    satisfies_c(A), satisfies_d(A), p)"
    by (simp add: satisfies_formula_def satisfies_a_def satisfies_b_def
                  satisfies_c_def satisfies_d_def)

    text{*Further constraints on the class @{term M} in order to prove
          absoluteness for the constants defined above.  The ultimate goal
          is the absoluteness of the function @{term satisfies}. *}
    locale M_satisfies = M_eclose +
     assumes
       Member_replacement:
        "[|M(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (M, λenv z. ∃bo[M]. ∃nx[M]. ∃ny[M].
                  env ∈ list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) &
                  is_bool_of_o(M, nx ∈ ny, bo) &
                  pair(M, env, bo, z))"
     and
       Equal_replacement:
        "[|M(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (M, λenv z. ∃bo[M]. ∃nx[M]. ∃ny[M].
                  env ∈ list(A) & is_nth(M,x,env,nx) & is_nth(M,y,env,ny) &
                  is_bool_of_o(M, nx = ny, bo) &
                  pair(M, env, bo, z))"
     and
       Nand_replacement:
        "[|M(A); M(rp); M(rq)|]
         ==> strong_replacement
             (M, λenv z. ∃rpe[M]. ∃rqe[M]. ∃andpq[M]. ∃notpq[M].
                   fun_apply(M,rp,env,rpe) & fun_apply(M,rq,env,rqe) &
                   is_and(M,rpe,rqe,andpq) & is_not(M,andpq,notpq) &
                   env ∈ list(A) & pair(M, env, notpq, z))"
     and
      Forall_replacement:
       "[|M(A); M(rp)|]
        ==> strong_replacement
            (M, λenv z. ∃bo[M].
                  env ∈ list(A) &
                  is_bool_of_o (M,
                                ∀a[M]. ∀co[M]. ∀rpco[M].
                                   a∈A --> is_Cons(M,a,env,co) -->
                                   fun_apply(M,rp,co,rpco) --> number1(M, rpco),
                                bo) &
                  pair(M,env,bo,z))"
     and
      formula_rec_replacement:
          --{*For the @{term transrec}*}
       "[|n ∈ nat; M(A)|] ==> transrec_replacement(M, satisfies_MH(M,A), n)"
     and
      formula_rec_lambda_replacement:
          --{*For the @{text "λ-abstraction"} in the @{term transrec} body*}
       "[|M(g); M(A)|] ==>
        strong_replacement (M,
           λx y. mem_formula(M,x) &
                 (∃c[M]. is_formula_case(M, satisfies_is_a(M,A),
                                      satisfies_is_b(M,A),
                                      satisfies_is_c(M,A,g),
                                      satisfies_is_d(M,A,g), x, c) &
                 pair(M, x, c, y)))"

    lemma (in M_satisfies) Member_replacement':
        "[|M(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (M, λenv z. env ∈ list(A) &
                         z = ⟨env, bool_of_o(nth(x, env) ∈ nth(y, env))⟩)"
    by (insert Member_replacement, simp)

    lemma (in M_satisfies) Equal_replacement':
        "[|M(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (M, λenv z. env ∈ list(A) &
                         z = ⟨env, bool_of_o(nth(x, env) = nth(y, env))⟩)"
    by (insert Equal_replacement, simp)

    lemma (in M_satisfies) Nand_replacement':
        "[|M(A); M(rp); M(rq)|]
         ==> strong_replacement
             (M, λenv z. env ∈ list(A) & z = ⟨env, not(rp`env and rq`env)⟩)"
    by (insert Nand_replacement, simp)

    lemma (in M_satisfies) Forall_replacement':
       "[|M(A); M(rp)|]
        ==> strong_replacement
            (M, λenv z.
                   env ∈ list(A) &
                   z = ⟨env, bool_of_o (∀a∈A. rp ` Cons(a,env) = 1)⟩)"
    by (insert Forall_replacement, simp)

    lemma (in M_satisfies) a_closed:
         "[|M(A); x∈nat; y∈nat|] ==> M(satisfies_a(A,x,y))"
    apply (simp add: satisfies_a_def)
    apply (blast intro: lam_closed2 Member_replacement')
    done

    lemma (in M_satisfies) a_rel:
         "M(A) ==> Relation2(M, nat, nat, satisfies_is_a(M,A), satisfies_a(A))"
    apply (simp add: Relation2_def satisfies_is_a_def satisfies_a_def)
    apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
    done

    lemma (in M_satisfies) b_closed:
         "[|M(A); x∈nat; y∈nat|] ==> M(satisfies_b(A,x,y))"
    apply (simp add: satisfies_b_def)
    apply (blast intro: lam_closed2 Equal_replacement')
    done

    lemma (in M_satisfies) b_rel:
         "M(A) ==> Relation2(M, nat, nat, satisfies_is_b(M,A), satisfies_b(A))"
    apply (simp add: Relation2_def satisfies_is_b_def satisfies_b_def)
    apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
    done

    lemma (in M_satisfies) c_closed:
         "[|M(A); x ∈ formula; y ∈ formula; M(rx); M(ry)|]
          ==> M(satisfies_c(A,x,y,rx,ry))"
    apply (simp add: satisfies_c_def)
    apply (rule lam_closed2)
    apply (rule Nand_replacement')
    apply (simp_all add: formula_into_M list_into_M [of _ A])
    done

    lemma (in M_satisfies) c_rel:
     "[|M(A); M(f)|] ==>
      Relation2 (M, formula, formula,
                   satisfies_is_c(M,A,f),
                   λu v. satisfies_c(A, u, v, f ` succ(depth(u)) ` u,
                                              f ` succ(depth(v)) ` v))"
    apply (simp add: Relation2_def satisfies_is_c_def satisfies_c_def)
    apply (auto del: iffI intro!: lambda_abs2
                simp add: Relation1_def formula_into_M)
    done

    lemma (in M_satisfies) d_closed:
         "[|M(A); x ∈ formula; M(rx)|] ==> M(satisfies_d(A,x,rx))"
    apply (simp add: satisfies_d_def)
    apply (rule lam_closed2)
    apply (rule Forall_replacement')
    apply (simp_all add: formula_into_M list_into_M [of _ A])
    done

    lemma (in M_satisfies) d_rel:
     "[|M(A); M(f)|] ==>
      Relation1(M, formula, satisfies_is_d(M,A,f),
         λu. satisfies_d(A, u, f ` succ(depth(u)) ` u))"
    apply (simp del: rall_abs
                add: Relation1_def satisfies_is_d_def satisfies_d_def)
    apply (auto del: iffI intro!: lambda_abs2 simp add: Relation1_def)
    done

    lemma (in M_satisfies) fr_replace:
          "[|n ∈ nat; M(A)|] ==> transrec_replacement(M,satisfies_MH(M,A),n)"
    by (blast intro: formula_rec_replacement)

    lemma (in M_satisfies) formula_case_satisfies_closed:
     "[|M(g); M(A); x ∈ formula|] ==>
      M(formula_case (satisfies_a(A), satisfies_b(A),
           λu v. satisfies_c(A, u, v,
                             g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
           λu. satisfies_d (A, u, g ` succ(depth(u)) ` u),
           x))"
    by (blast intro: formula_case_closed a_closed b_closed c_closed d_closed)

    lemma (in M_satisfies) fr_lam_replace:
       "[|M(g); M(A)|] ==>
        strong_replacement (M, λx y. x ∈ formula &
                y = ⟨x,
                     formula_rec_case(satisfies_a(A),
                                      satisfies_b(A),
                                      satisfies_c(A),
                                      satisfies_d(A), g, x)⟩)"
    apply (insert formula_rec_lambda_replacement)
    apply (simp add: formula_rec_case_def formula_case_satisfies_closed
                     formula_case_abs [OF a_rel b_rel c_rel d_rel])
    done

    text{*Instantiate locale @{text Formula_Rec} for the
          Function @{term satisfies}*}

    lemma (in M_satisfies) Formula_Rec_axioms_M:
       "M(A) ==>
        Formula_Rec_axioms(M, satisfies_a(A), satisfies_is_a(M,A),
                              satisfies_b(A), satisfies_is_b(M,A),
                              satisfies_c(A), satisfies_is_c(M,A),
                              satisfies_d(A), satisfies_is_d(M,A))"
    apply (rule Formula_Rec_axioms.intro)
    apply (assumption |
           rule a_closed a_rel b_closed b_rel c_closed c_rel d_closed d_rel
           fr_replace [unfolded satisfies_MH_def]
           fr_lam_replace) +
    done

    theorem (in M_satisfies) Formula_Rec_M:
        "M(A) ==>
         PROP Formula_Rec(M, satisfies_a(A), satisfies_is_a(M,A),
                             satisfies_b(A), satisfies_is_b(M,A),
                             satisfies_c(A), satisfies_is_c(M,A),
                             satisfies_d(A), satisfies_is_d(M,A))"
    apply (rule Formula_Rec.intro, assumption+)
    apply (erule Formula_Rec_axioms_M)
    done

    lemmas (in M_satisfies)
        satisfies_closed' = Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
    and satisfies_abs'    = Formula_Rec.formula_rec_abs [OF Formula_Rec_M]

    lemma (in M_satisfies) satisfies_closed:
      "[|M(A); p ∈ formula|] ==> M(satisfies(A,p))"
    by (simp add: Formula_Rec.formula_rec_closed [OF Formula_Rec_M]
                  satisfies_eq)

    lemma (in M_satisfies) satisfies_abs:
      "[|M(A); M(z); p ∈ formula|]
       ==> is_satisfies(M,A,p,z) <-> z = satisfies(A,p)"
    by (simp only: Formula_Rec.formula_rec_abs [OF Formula_Rec_M]
                   satisfies_eq is_satisfies_def satisfies_MH_def)

    subsection{*Internalizations Needed to Instantiate @{text "M_satisfies"}*}

    subsubsection{*The Operator @{term is_depth_apply}, Internalized*}

    (* is_depth_apply(M,h,p,z) ==
        ∃dp[M]. ∃sdp[M]. ∃hsdp[M].
          2        1         0
            finite_ordinal(M,dp) & is_depth(M,p,dp) & successor(M,dp,sdp) &
            fun_apply(M,h,sdp,hsdp) & fun_apply(M,hsdp,p,z) *)
    constdefs depth_apply_fm :: "[i,i,i]=>i"
        "depth_apply_fm(h,p,z) ==
           Exists(Exists(Exists(
            And(finite_ordinal_fm(2),
             And(depth_fm(p#+3,2),
              And(succ_fm(2,1),
               And(fun_apply_fm(h#+3,1,0), fun_apply_fm(0,p#+3,z#+3))))))))"

    lemma depth_apply_type [TC]:
         "[| x ∈ nat; y ∈ nat; z ∈ nat |] ==> depth_apply_fm(x,y,z) ∈ formula"
    by (simp add: depth_apply_fm_def)

    lemma sats_depth_apply_fm [simp]:
       "[| x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
        ==> sats(A, depth_apply_fm(x,y,z), env) <->
            is_depth_apply(##A, nth(x,env), nth(y,env), nth(z,env))"
    by (simp add: depth_apply_fm_def is_depth_apply_def)

    lemma depth_apply_iff_sats:
        "[| nth(i,env) = x; nth(j,env) = y; nth(k,env) = z;
            i ∈ nat; j ∈ nat; k ∈ nat; env ∈ list(A)|]
         ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i,j,k), env)"
    by simp

    lemma depth_apply_reflection:
         "REFLECTS[λx. is_depth_apply(L,f(x),g(x),h(x)),
                   λi x. is_depth_apply(##Lset(i),f(x),g(x),h(x))]"
    apply (simp only: is_depth_apply_def)
    apply (intro FOL_reflections function_reflections depth_reflection
                 finite_ordinal_reflection)
    done

    subsubsection{*The Operator @{term satisfies_is_a}, Internalized*}

    (* satisfies_is_a(M,A) ==
        λx y zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. is_bool_of_o(M,
                          ∃nx[M]. ∃ny[M].
                           is_nth(M,x,env,nx) & is_nth(M,y,env,ny) & nx ∈ ny, z),
                    zz)  *)

    constdefs satisfies_is_a_fm :: "[i,i,i,i]=>i"
     "satisfies_is_a_fm(A,x,y,z) ==
       Forall(
         Implies(is_list_fm(succ(A),0),
           lambda_fm(
             bool_of_o_fm(Exists(
                           Exists(And(nth_fm(x#+6,3,1),
                                   And(nth_fm(y#+6,3,0),
                                       Member(1,0))))), 0),
             0, succ(z))))"

    lemma satisfies_is_a_type [TC]:
         "[| A ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
          ==> satisfies_is_a_fm(A,x,y,z) ∈ formula"
    by (simp add: satisfies_is_a_fm_def)

    lemma sats_satisfies_is_a_fm [simp]:
       "[| u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)|]
        ==> sats(A, satisfies_is_a_fm(u,x,y,z), env) <->
            satisfies_is_a(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    apply (frule_tac x=x in lt_length_in_nat, assumption)
    apply (frule_tac x=y in lt_length_in_nat, assumption)
    apply (simp add: satisfies_is_a_fm_def satisfies_is_a_def sats_lambda_fm
                     sats_bool_of_o_fm)
    done

    lemma satisfies_is_a_iff_sats:
      "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
          u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)|]
       ==> satisfies_is_a(##A,nu,nx,ny,nz) <->
           sats(A, satisfies_is_a_fm(u,x,y,z), env)"
    by simp

    theorem satisfies_is_a_reflection:
         "REFLECTS[λx. satisfies_is_a(L,f(x),g(x),h(x),g'(x)),
                   λi x. satisfies_is_a(##Lset(i),f(x),g(x),h(x),g'(x))]"
    apply (unfold satisfies_is_a_def)
    apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
                 nth_reflection is_list_reflection)
    done

    subsubsection{*The Operator @{term satisfies_is_b}, Internalized*}

    (* satisfies_is_b(M,A) ==
        λx y zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. is_bool_of_o(M,
                          ∃nx[M]. is_nth(M,x,env,nx) & is_nth(M,y,env,nx), z),
                    zz) *)

    constdefs satisfies_is_b_fm :: "[i,i,i,i]=>i"
     "satisfies_is_b_fm(A,x,y,z) ==
       Forall(
         Implies(is_list_fm(succ(A),0),
           lambda_fm(
             bool_of_o_fm(Exists(And(nth_fm(x#+5,2,0), nth_fm(y#+5,2,0))), 0),
             0, succ(z))))"

    lemma satisfies_is_b_type [TC]:
         "[| A ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
          ==> satisfies_is_b_fm(A,x,y,z) ∈ formula"
    by (simp add: satisfies_is_b_fm_def)

    lemma sats_satisfies_is_b_fm [simp]:
       "[| u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)|]
        ==> sats(A, satisfies_is_b_fm(u,x,y,z), env) <->
            satisfies_is_b(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    apply (frule_tac x=x in lt_length_in_nat, assumption)
    apply (frule_tac x=y in lt_length_in_nat, assumption)
    apply (simp add: satisfies_is_b_fm_def satisfies_is_b_def sats_lambda_fm
                     sats_bool_of_o_fm)
    done

    lemma satisfies_is_b_iff_sats:
      "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
          u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A)|]
       ==> satisfies_is_b(##A,nu,nx,ny,nz) <->
           sats(A, satisfies_is_b_fm(u,x,y,z), env)"
    by simp

    theorem satisfies_is_b_reflection:
         "REFLECTS[λx. satisfies_is_b(L,f(x),g(x),h(x),g'(x)),
                   λi x. satisfies_is_b(##Lset(i),f(x),g(x),h(x),g'(x))]"
    apply (unfold satisfies_is_b_def)
    apply (intro FOL_reflections is_lambda_reflection bool_of_o_reflection
                 nth_reflection is_list_reflection)
    done

    subsubsection{*The Operator @{term satisfies_is_c}, Internalized*}

    (* satisfies_is_c(M,A,h) ==
        λp q zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA, λenv z. ∃hp[M]. ∃hq[M].
                     (∃rp[M]. is_depth_apply(M,h,p,rp) & fun_apply(M,rp,env,hp)) &
                     (∃rq[M]. is_depth_apply(M,h,q,rq) & fun_apply(M,rq,env,hq)) &
                     (∃pq[M]. is_and(M,hp,hq,pq) & is_not(M,pq,z)),
                    zz) *)

    constdefs satisfies_is_c_fm :: "[i,i,i,i,i]=>i"
     "satisfies_is_c_fm(A,h,p,q,zz) ==
       Forall(
         Implies(is_list_fm(succ(A),0),
           lambda_fm(
             Exists(Exists(
              And(Exists(And(depth_apply_fm(h#+7,p#+7,0), fun_apply_fm(0,4,2))),
              And(Exists(And(depth_apply_fm(h#+7,q#+7,0), fun_apply_fm(0,4,1))),
                  Exists(And(and_fm(2,1,0), not_fm(0,3))))))),
             0, succ(zz))))"

    lemma satisfies_is_c_type [TC]:
         "[| A ∈ nat; h ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
          ==> satisfies_is_c_fm(A,h,x,y,z) ∈ formula"
    by (simp add: satisfies_is_c_fm_def)

    lemma sats_satisfies_is_c_fm [simp]:
       "[| u ∈ nat; v ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
        ==> sats(A, satisfies_is_c_fm(u,v,x,y,z), env) <->
            satisfies_is_c(##A, nth(u,env), nth(v,env), nth(x,env),
                                nth(y,env), nth(z,env))"
    by (simp add: satisfies_is_c_fm_def satisfies_is_c_def sats_lambda_fm)

    lemma satisfies_is_c_iff_sats:
      "[| nth(u,env) = nu; nth(v,env) = nv; nth(x,env) = nx; nth(y,env) = ny;
          nth(z,env) = nz;
          u ∈ nat; v ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
       ==> satisfies_is_c(##A,nu,nv,nx,ny,nz) <->
           sats(A, satisfies_is_c_fm(u,v,x,y,z), env)"
    by simp

    theorem satisfies_is_c_reflection:
         "REFLECTS[λx. satisfies_is_c(L,f(x),g(x),h(x),g'(x),h'(x)),
                   λi x. satisfies_is_c(##Lset(i),f(x),g(x),h(x),g'(x),h'(x))]"
    apply (unfold satisfies_is_c_def)
    apply (intro FOL_reflections function_reflections is_lambda_reflection
                 extra_reflections nth_reflection depth_apply_reflection
                 is_list_reflection)
    done

    subsubsection{*The Operator @{term satisfies_is_d}, Internalized*}

    (* satisfies_is_d(M,A,h) ==
        λp zz. ∀lA[M]. is_list(M,A,lA) -->
                 is_lambda(M, lA,
                    λenv z. ∃rp[M]. is_depth_apply(M,h,p,rp) &
                        is_bool_of_o(M,
                               ∀x[M]. ∀xenv[M]. ∀hp[M].
                                  x∈A --> is_Cons(M,x,env,xenv) -->
                                  fun_apply(M,rp,xenv,hp) --> number1(M,hp),
                      z),
                   zz) *)

    constdefs satisfies_is_d_fm :: "[i,i,i,i]=>i"
     "satisfies_is_d_fm(A,h,p,zz) ==
       Forall(
         Implies(is_list_fm(succ(A),0),
           lambda_fm(
             Exists(
               And(depth_apply_fm(h#+5,p#+5,0),
                   bool_of_o_fm(
                    Forall(Forall(Forall(
                     Implies(Member(2,A#+8),
                      Implies(Cons_fm(2,5,1),
                       Implies(fun_apply_fm(3,1,0), number1_fm(0))))))), 1))),
             0, succ(zz))))"

    lemma satisfies_is_d_type [TC]:
         "[| A ∈ nat; h ∈ nat; x ∈ nat; z ∈ nat |]
          ==> satisfies_is_d_fm(A,h,x,z) ∈ formula"
    by (simp add: satisfies_is_d_fm_def)

    lemma sats_satisfies_is_d_fm [simp]:
       "[| u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
        ==> sats(A, satisfies_is_d_fm(u,x,y,z), env) <->
            satisfies_is_d(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    by (simp add: satisfies_is_d_fm_def satisfies_is_d_def sats_lambda_fm
                  sats_bool_of_o_fm)

    lemma satisfies_is_d_iff_sats:
      "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
          u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
       ==> satisfies_is_d(##A,nu,nx,ny,nz) <->
           sats(A, satisfies_is_d_fm(u,x,y,z), env)"
    by simp

    theorem satisfies_is_d_reflection:
         "REFLECTS[λx. satisfies_is_d(L,f(x),g(x),h(x),g'(x)),
                   λi x. satisfies_is_d(##Lset(i),f(x),g(x),h(x),g'(x))]"
    apply (unfold satisfies_is_d_def)
    apply (intro FOL_reflections function_reflections is_lambda_reflection
                 extra_reflections nth_reflection depth_apply_reflection
                 is_list_reflection)
    done

    subsubsection{*The Operator @{term satisfies_MH}, Internalized*}

    (* satisfies_MH ==
        λM A u f zz.
             ∀fml[M]. is_formula(M,fml) -->
                 is_lambda (M, fml,
                   is_formula_case (M, satisfies_is_a(M,A),
                                    satisfies_is_b(M,A),
                                    satisfies_is_c(M,A,f), satisfies_is_d(M,A,f)),
                   zz) *)

    constdefs satisfies_MH_fm :: "[i,i,i,i]=>i"
     "satisfies_MH_fm(A,u,f,zz) ==
       Forall(
         Implies(is_formula_fm(0),
           lambda_fm(
             formula_case_fm(satisfies_is_a_fm(A#+7,2,1,0),
                             satisfies_is_b_fm(A#+7,2,1,0),
                             satisfies_is_c_fm(A#+7,f#+7,2,1,0),
                             satisfies_is_d_fm(A#+6,f#+6,1,0),
                             1, 0),
             0, succ(zz))))"

    lemma satisfies_MH_type [TC]:
         "[| A ∈ nat; u ∈ nat; x ∈ nat; z ∈ nat |]
          ==> satisfies_MH_fm(A,u,x,z) ∈ formula"
    by (simp add: satisfies_MH_fm_def)

    lemma sats_satisfies_MH_fm [simp]:
       "[| u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
        ==> sats(A, satisfies_MH_fm(u,x,y,z), env) <->
            satisfies_MH(##A, nth(u,env), nth(x,env), nth(y,env), nth(z,env))"
    by (simp add: satisfies_MH_fm_def satisfies_MH_def sats_lambda_fm
                  sats_formula_case_fm)

    lemma satisfies_MH_iff_sats:
      "[| nth(u,env) = nu; nth(x,env) = nx; nth(y,env) = ny; nth(z,env) = nz;
          u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A)|]
       ==> satisfies_MH(##A,nu,nx,ny,nz) <->
           sats(A, satisfies_MH_fm(u,x,y,z), env)"
    by simp

    lemmas satisfies_reflections =
           is_lambda_reflection is_formula_reflection
           is_formula_case_reflection
           satisfies_is_a_reflection satisfies_is_b_reflection
           satisfies_is_c_reflection satisfies_is_d_reflection

    theorem satisfies_MH_reflection:
         "REFLECTS[λx. satisfies_MH(L,f(x),g(x),h(x),g'(x)),
                   λi x. satisfies_MH(##Lset(i),f(x),g(x),h(x),g'(x))]"
    apply (unfold satisfies_MH_def)
    apply (intro FOL_reflections satisfies_reflections)
    done

    subsection{*Lemmas for Instantiating the Locale @{text "M_satisfies"}*}

    subsubsection{*The @{term "Member"} Case*}

    lemma Member_Reflects:
     "REFLECTS[λu. ∃v[L]. v ∈ B ∧ (∃bo[L]. ∃nx[L]. ∃ny[L].
              v ∈ lstA ∧ is_nth(L,x,v,nx) ∧ is_nth(L,y,v,ny) ∧
              is_bool_of_o(L, nx ∈ ny, bo) ∧ pair(L,v,bo,u)),
       λi u. ∃v ∈ Lset(i). v ∈ B ∧ (∃bo ∈ Lset(i). ∃nx ∈ Lset(i). ∃ny ∈ Lset(i).
                 v ∈ lstA ∧ is_nth(##Lset(i), x, v, nx) ∧
                 is_nth(##Lset(i), y, v, ny) ∧
              is_bool_of_o(##Lset(i), nx ∈ ny, bo) ∧ pair(##Lset(i), v, bo, u))]"
    by (intro FOL_reflections function_reflections nth_reflection
              bool_of_o_reflection)

    lemma Member_replacement:
        "[|L(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (L, λenv z. ∃bo[L]. ∃nx[L]. ∃ny[L].
                  env ∈ list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) &
                  is_bool_of_o(L, nx ∈ ny, bo) &
                  pair(L, env, bo, z))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{list(A),B,x,y}"
             in gen_separation_multi [OF Member_Reflects],
           auto simp add: nat_into_M list_closed)
    apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
    apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    done

    subsubsection{*The @{term "Equal"} Case*}

    lemma Equal_Reflects:
     "REFLECTS[λu. ∃v[L]. v ∈ B ∧ (∃bo[L]. ∃nx[L]. ∃ny[L].
              v ∈ lstA ∧ is_nth(L, x, v, nx) ∧ is_nth(L, y, v, ny) ∧
              is_bool_of_o(L, nx = ny, bo) ∧ pair(L, v, bo, u)),
       λi u. ∃v ∈ Lset(i). v ∈ B ∧ (∃bo ∈ Lset(i). ∃nx ∈ Lset(i). ∃ny ∈ Lset(i).
                 v ∈ lstA ∧ is_nth(##Lset(i), x, v, nx) ∧
                 is_nth(##Lset(i), y, v, ny) ∧
              is_bool_of_o(##Lset(i), nx = ny, bo) ∧ pair(##Lset(i), v, bo, u))]"
    by (intro FOL_reflections function_reflections nth_reflection
              bool_of_o_reflection)

    lemma Equal_replacement:
        "[|L(A); x ∈ nat; y ∈ nat|]
         ==> strong_replacement
             (L, λenv z. ∃bo[L]. ∃nx[L]. ∃ny[L].
                  env ∈ list(A) & is_nth(L,x,env,nx) & is_nth(L,y,env,ny) &
                  is_bool_of_o(L, nx = ny, bo) &
                  pair(L, env, bo, z))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{list(A),B,x,y}"
             in gen_separation_multi [OF Equal_Reflects],
           auto simp add: nat_into_M list_closed)
    apply (rule_tac env="[list(A),B,x,y]" in DPow_LsetI)
    apply (rule sep_rules nth_iff_sats is_bool_of_o_iff_sats | simp)+
    done

    subsubsection{*The @{term "Nand"} Case*}

    lemma Nand_Reflects:
        "REFLECTS [λx. ∃u[L]. u ∈ B ∧
                   (∃rpe[L]. ∃rqe[L]. ∃andpq[L]. ∃notpq[L].
                     fun_apply(L, rp, u, rpe) ∧ fun_apply(L, rq, u, rqe) ∧
                     is_and(L, rpe, rqe, andpq) ∧ is_not(L, andpq, notpq) ∧
                     u ∈ list(A) ∧ pair(L, u, notpq, x)),
        λi x. ∃u ∈ Lset(i). u ∈ B ∧
         (∃rpe ∈ Lset(i). ∃rqe ∈ Lset(i). ∃andpq ∈ Lset(i). ∃notpq ∈ Lset(i).
           fun_apply(##Lset(i), rp, u, rpe) ∧ fun_apply(##Lset(i), rq, u, rqe) ∧
           is_and(##Lset(i), rpe, rqe, andpq) ∧ is_not(##Lset(i), andpq, notpq) ∧
           u ∈ list(A) ∧ pair(##Lset(i), u, notpq, x))]"
    apply (unfold is_and_def is_not_def)
    apply (intro FOL_reflections function_reflections)
    done

    lemma Nand_replacement:
        "[|L(A); L(rp); L(rq)|]
         ==> strong_replacement
             (L, λenv z. ∃rpe[L]. ∃rqe[L]. ∃andpq[L]. ∃notpq[L].
                   fun_apply(L,rp,env,rpe) & fun_apply(L,rq,env,rqe) &
                   is_and(L,rpe,rqe,andpq) & is_not(L,andpq,notpq) &
                   env ∈ list(A) & pair(L, env, notpq, z))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{list(A),B,rp,rq}"
             in gen_separation_multi [OF Nand_Reflects],
           auto simp add: list_closed)
    apply (rule_tac env="[list(A),B,rp,rq]" in DPow_LsetI)
    apply (rule sep_rules is_and_iff_sats is_not_iff_sats | simp)+
    done

    subsubsection{*The @{term "Forall"} Case*}

    lemma Forall_Reflects:
     "REFLECTS [λx. ∃u[L]. u ∈ B ∧ (∃bo[L]. u ∈ list(A) ∧
                     is_bool_of_o (L,
         ∀a[L]. ∀co[L]. ∀rpco[L]. a ∈ A -->
                    is_Cons(L,a,u,co) --> fun_apply(L,rp,co,rpco) -->
                    number1(L,rpco),
                               bo) ∧ pair(L,u,bo,x)),
     λi x. ∃u ∈ Lset(i). u ∈ B ∧ (∃bo ∈ Lset(i). u ∈ list(A) ∧
            is_bool_of_o (##Lset(i),
     ∀a ∈ Lset(i). ∀co ∈ Lset(i). ∀rpco ∈ Lset(i). a ∈ A -->
                is_Cons(##Lset(i),a,u,co) --> fun_apply(##Lset(i),rp,co,rpco) -->
                number1(##Lset(i),rpco),
                           bo) ∧ pair(##Lset(i),u,bo,x))]"
    apply (unfold is_bool_of_o_def)
    apply (intro FOL_reflections function_reflections Cons_reflection)
    done

    lemma Forall_replacement:
       "[|L(A); L(rp)|]
        ==> strong_replacement
            (L, λenv z. ∃bo[L].
                  env ∈ list(A) &
                  is_bool_of_o (L,
                                ∀a[L]. ∀co[L]. ∀rpco[L].
                                   a∈A --> is_Cons(L,a,env,co) -->
                                   fun_apply(L,rp,co,rpco) --> number1(L, rpco),
                                bo) &
                  pair(L,env,bo,z))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{A,list(A),B,rp}"
             in gen_separation_multi [OF Forall_Reflects],
           auto simp add: list_closed)
    apply (rule_tac env="[A,list(A),B,rp]" in DPow_LsetI)
    apply (rule sep_rules is_bool_of_o_iff_sats Cons_iff_sats | simp)+
    done

    subsubsection{*The @{term "transrec_replacement"} Case*}

    lemma formula_rec_replacement_Reflects:
     "REFLECTS [λx. ∃u[L]. u ∈ B ∧ (∃y[L]. pair(L, u, y, x) ∧
                 is_wfrec (L, satisfies_MH(L,A), mesa, u, y)),
        λi x. ∃u ∈ Lset(i). u ∈ B ∧ (∃y ∈ Lset(i). pair(##Lset(i), u, y, x) ∧
                 is_wfrec (##Lset(i), satisfies_MH(##Lset(i),A), mesa, u, y))]"
    by (intro FOL_reflections function_reflections satisfies_MH_reflection
              is_wfrec_reflection)

    lemma formula_rec_replacement:
          --{*For the @{term transrec}*}
       "[|n ∈ nat; L(A)|] ==> transrec_replacement(L, satisfies_MH(L,A), n)"
    apply (rule transrec_replacementI, simp add: nat_into_M)
    apply (rule strong_replacementI)
    apply (rule_tac u="{B,A,n,Memrel(eclose({n}))}"
             in gen_separation_multi [OF formula_rec_replacement_Reflects],
           auto simp add: nat_into_M)
    apply (rule_tac env="[B,A,n,Memrel(eclose({n}))]" in DPow_LsetI)
    apply (rule sep_rules satisfies_MH_iff_sats is_wfrec_iff_sats | simp)+
    done

    subsubsection{*The Lambda Replacement Case*}

    lemma formula_rec_lambda_replacement_Reflects:
     "REFLECTS [λx. ∃u[L]. u ∈ B &
         mem_formula(L,u) &
         (∃c[L].
             is_formula_case
              (L, satisfies_is_a(L,A), satisfies_is_b(L,A),
               satisfies_is_c(L,A,g), satisfies_is_d(L,A,g),
               u, c) &
             pair(L,u,c,x)),
      λi x. ∃u ∈ Lset(i). u ∈ B & mem_formula(##Lset(i),u) &
         (∃c ∈ Lset(i).
             is_formula_case
              (##Lset(i), satisfies_is_a(##Lset(i),A), satisfies_is_b(##Lset(i),A),
               satisfies_is_c(##Lset(i),A,g), satisfies_is_d(##Lset(i),A,g),
               u, c) &
             pair(##Lset(i),u,c,x))]"
    by (intro FOL_reflections function_reflections mem_formula_reflection
              is_formula_case_reflection satisfies_is_a_reflection
              satisfies_is_b_reflection satisfies_is_c_reflection
              satisfies_is_d_reflection)

    lemma formula_rec_lambda_replacement:
          --{*For the @{term transrec}*}
       "[|L(g); L(A)|] ==>
        strong_replacement (L,
           λx y. mem_formula(L,x) &
                 (∃c[L]. is_formula_case(L, satisfies_is_a(L,A),
                                      satisfies_is_b(L,A),
                                      satisfies_is_c(L,A,g),
                                      satisfies_is_d(L,A,g), x, c) &
                 pair(L, x, c, y)))"
    apply (rule strong_replacementI)
    apply (rule_tac u="{B,A,g}"
             in gen_separation_multi [OF formula_rec_lambda_replacement_Reflects],
           auto)
    apply (rule_tac env="[A,g,B]" in DPow_LsetI)
    apply (rule sep_rules mem_formula_iff_sats
              formula_case_iff_sats satisfies_is_a_iff_sats
              satisfies_is_b_iff_sats satisfies_is_c_iff_sats
              satisfies_is_d_iff_sats | simp)+
    done

    subsection{*Instantiating @{text M_satisfies}*}

    lemma M_satisfies_axioms_L: "M_satisfies_axioms(L)"
      apply (rule M_satisfies_axioms.intro)
           apply (assumption | rule
             Member_replacement Equal_replacement
             Nand_replacement Forall_replacement
             formula_rec_replacement formula_rec_lambda_replacement)+
      done

    theorem M_satisfies_L: "PROP M_satisfies(L)"
    apply (rule M_satisfies.intro)
         apply (rule M_eclose.axioms [OF M_eclose_L])+
    apply (rule M_satisfies_axioms_L)
    done

    text{*Finally: the point of the whole theory!*}
    lemmas satisfies_closed = M_satisfies.satisfies_closed [OF M_satisfies_L]
       and satisfies_abs = M_satisfies.satisfies_abs [OF M_satisfies_L]

    end

### More Internalization

#### The Formula @{term is_depth}, Internalized

lemma depth_fm_type:

      [| x ∈ nat; y ∈ nat |] ==> depth_fm(x, y) ∈ formula

lemma sats_depth_fm:

      [| x ∈ nat; y < length(env); env ∈ list(A) |]
      ==> sats(A, depth_fm(x, y), env) <-> is_depth(##A, nth(x, env), nth(y, env))

lemma depth_iff_sats:

      [| nth(i, env) = x; nth(j, env) = y; i ∈ nat; j < length(env); env ∈ list(A) |]
      ==> is_depth(##A, x, y) <-> sats(A, depth_fm(i, j), env)

theorem depth_reflection:

      REFLECTS [%x. is_depth(L, f(x), g(x)), %i x. is_depth(##Lset(i), f(x), g(x))]

#### The Operator @{term is_formula_case}

lemma is_formula_case_type:

      [| is_a ∈ formula; is_b ∈ formula; is_c ∈ formula; is_d ∈ formula; x ∈ nat;
         y ∈ nat |]
      ==> formula_case_fm(is_a, is_b, is_c, is_d, x, y) ∈ formula

lemma sats_formula_case_fm:

      [| !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1.
            [| a0 ∈ A; a1 ∈ A |]
            ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0, Cons(a1, env)));
         x ∈ nat; y < length(env); env ∈ list(A) |]
      ==> sats(A, formula_case_fm(is_a, is_b, is_c, is_d, x, y), env) <->
          is_formula_case(##A, ISA, ISB, ISC, ISD, nth(x, env), nth(y, env))

lemma formula_case_iff_sats:

      [| !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISA(a2, a1, a0) <-> sats(A, is_a, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISB(a2, a1, a0) <-> sats(A, is_b, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1 a2.
            [| a0 ∈ A; a1 ∈ A; a2 ∈ A |]
            ==> ISC(a2, a1, a0) <-> sats(A, is_c, Cons(a0, Cons(a1, Cons(a2, env))));
         !!a0 a1.
            [| a0 ∈ A; a1 ∈ A |]
            ==> ISD(a1, a0) <-> sats(A, is_d, Cons(a0, Cons(a1, env)));
         nth(i, env) = x; nth(j, env) = y; i ∈ nat; j < length(env); env ∈ list(A) |]
      ==> is_formula_case(##A, ISA, ISB, ISC, ISD, x, y) <->
          sats(A, formula_case_fm(is_a, is_b, is_c, is_d, i, j), env)

theorem is_formula_case_reflection:

      [| !!h f g g'.
            REFLECTS [%x. is_a(L, h(x), f(x), g(x), g'(x)),
               %i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_b(L, h(x), f(x), g(x), g'(x)),
               %i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_c(L, h(x), f(x), g(x), g'(x)),
               %i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_d(L, h(x), f(x), g(x)),
               %i x. is_d(##Lset(i), h(x), f(x), g(x))] |]
      ==> REFLECTS
             [%x. is_formula_case
                   (L, is_a(L, x), is_b(L, x), is_c(L, x), is_d(L, x), g(x), h(x)),
             %i x. is_formula_case
                    (##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x),
                     is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]

### Absoluteness for the Function @{term satisfies}

lemma is_depth_apply_abs:

      [| PROP M_datatypes(M); M(h); p ∈ formula; M(z) |]
      ==> is_depth_apply(M, h, p, z) <-> z = h ` succ(depth(p)) ` p

lemma satisfies_eq:

      satisfies(A, p) =
      formula_rec(satisfies_a(A), satisfies_b(A), satisfies_c(A), satisfies_d(A), p)

lemma Member_replacement':

      [| PROP M_satisfies(M); M(A); x ∈ nat; y ∈ nat |]
      ==> strong_replacement
           (M, %env z.
                  env ∈ list(A) ∧ z = ⟨env, bool_of_o(nth(x, env) ∈ nth(y, env))⟩)

lemma Equal_replacement':

      [| PROP M_satisfies(M); M(A); x ∈ nat; y ∈ nat |]
      ==> strong_replacement
           (M, %env z.
                  env ∈ list(A) ∧ z = ⟨env, bool_of_o(nth(x, env) = nth(y, env))⟩)

lemma Nand_replacement':

      [| PROP M_satisfies(M); M(A); M(rp); M(rq) |]
      ==> strong_replacement
           (M, %env z. env ∈ list(A) ∧ z = ⟨env, not(rp ` env and rq ` env)⟩)

lemma Forall_replacement':

      [| PROP M_satisfies(M); M(A); M(rp) |]
      ==> strong_replacement
           (M, %env z.
                  env ∈ list(A) ∧ z = ⟨env, bool_of_o(∀a∈A. rp ` Cons(a, env) = 1)⟩)

lemma a_closed:

      [| PROP M_satisfies(M); M(A); x ∈ nat; y ∈ nat |] ==> M(satisfies_a(A, x, y))

lemma a_rel:

      [| PROP M_satisfies(M); M(A) |]
      ==> Relation2(M, nat, nat, satisfies_is_a(M, A), satisfies_a(A))

lemma b_closed:

      [| PROP M_satisfies(M); M(A); x ∈ nat; y ∈ nat |] ==> M(satisfies_b(A, x, y))

lemma b_rel:

      [| PROP M_satisfies(M); M(A) |]
      ==> Relation2(M, nat, nat, satisfies_is_b(M, A), satisfies_b(A))

lemma c_closed:

      [| PROP M_satisfies(M); M(A); x ∈ formula; y ∈ formula; M(rx); M(ry) |]
      ==> M(satisfies_c(A, x, y, rx, ry))

lemma c_rel:

      [| PROP M_satisfies(M); M(A); M(f) |]
      ==> Relation2
           (M, formula, formula, satisfies_is_c(M, A, f),
            %u v. satisfies_c
                   (A, u, v, f ` succ(depth(u)) ` u, f ` succ(depth(v)) ` v))

lemma d_closed:

      [| PROP M_satisfies(M); M(A); x ∈ formula; M(rx) |] ==> M(satisfies_d(A, x, rx))

lemma d_rel:

      [| PROP M_satisfies(M); M(A); M(f) |]
      ==> Relation1
           (M, formula, satisfies_is_d(M, A, f),
            %u. satisfies_d(A, u, f ` succ(depth(u)) ` u))

lemma fr_replace:

      [| PROP M_satisfies(M); n ∈ nat; M(A) |]
      ==> transrec_replacement(M, satisfies_MH(M, A), n)

lemma formula_case_satisfies_closed:

      [| PROP M_satisfies(M); M(g); M(A); x ∈ formula |]
      ==> M(formula_case
             (satisfies_a(A), satisfies_b(A),
              %u v. satisfies_c
                     (A, u, v, g ` succ(depth(u)) ` u, g ` succ(depth(v)) ` v),
              %u. satisfies_d(A, u, g ` succ(depth(u)) ` u), x))

lemma fr_lam_replace:

      [| PROP M_satisfies(M); M(g); M(A) |]
      ==> strong_replacement
           (M, %x y. x ∈ formula ∧
                     y = ⟨x, formula_rec_case
                              (satisfies_a(A), satisfies_b(A), satisfies_c(A),
                               satisfies_d(A), g, x)⟩)

lemma Formula_Rec_axioms_M:

      [| PROP M_satisfies(M); M(A) |]
      ==> Formula_Rec_axioms
           (M, satisfies_a(A), satisfies_is_a(M, A), satisfies_b(A),
            satisfies_is_b(M, A), satisfies_c(A), satisfies_is_c(M, A),
            satisfies_d(A), satisfies_is_d(M, A))

theorem Formula_Rec_M:

      [| PROP M_satisfies(M); M(A) |]
      ==> PROP Formula_Rec
                (M, satisfies_a(A), satisfies_is_a(M, A), satisfies_b(A),
                 satisfies_is_b(M, A), satisfies_c(A), satisfies_is_c(M, A),
                 satisfies_d(A), satisfies_is_d(M, A))

lemmas satisfies_closed':

      [| PROP M_satisfies(M); M(A); p ∈ formula |]
      ==> M(formula_rec
             (satisfies_a(A), satisfies_b(A), satisfies_c(A), satisfies_d(A), p))

and satisfies_abs':

      [| PROP M_satisfies(M); M(A); p ∈ formula; M(z) |]
      ==> is_formula_rec
           (M, %u f z.
                  ∀fml[M].
                     is_formula(M, fml) -->
                     is_lambda
                      (M, fml,
                       is_formula_case
                        (M, satisfies_is_a(M, A), satisfies_is_b(M, A),
                         satisfies_is_c(M, A, f), satisfies_is_d(M, A, f)),
                       z),
            p, z) <->
          z = formula_rec
               (satisfies_a(A), satisfies_b(A), satisfies_c(A), satisfies_d(A), p)

lemma satisfies_closed:

      [| PROP M_satisfies(M); M(A); p ∈ formula |] ==> M(satisfies(A, p))

lemma satisfies_abs:

      [| PROP M_satisfies(M); M(A); M(z); p ∈ formula |]
      ==> is_satisfies(M, A, p, z) <-> z = satisfies(A, p)

### Internalizations Needed to Instantiate @{text "M_satisfies"}

#### The Operator @{term is_depth_apply}, Internalized

lemma depth_apply_type:

      [| x ∈ nat; y ∈ nat; z ∈ nat |] ==> depth_apply_fm(x, y, z) ∈ formula

lemma sats_depth_apply_fm:

      [| x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> sats(A, depth_apply_fm(x, y, z), env) <->
          is_depth_apply(##A, nth(x, env), nth(y, env), nth(z, env))

lemma depth_apply_iff_sats:

      [| nth(i, env) = x; nth(j, env) = y; nth(k, env) = z; i ∈ nat; j ∈ nat; k ∈ nat;
         env ∈ list(A) |]
      ==> is_depth_apply(##A, x, y, z) <-> sats(A, depth_apply_fm(i, j, k), env)

lemma depth_apply_reflection:

      REFLECTS [%x. is_depth_apply(L, f(x), g(x), h(x)),
         %i x. is_depth_apply(##Lset(i), f(x), g(x), h(x))]

#### The Operator @{term satisfies_is_a}, Internalized

lemma satisfies_is_a_type:

      [| A ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
      ==> satisfies_is_a_fm(A, x, y, z) ∈ formula

lemma sats_satisfies_is_a_fm:

      [| u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A) |]
      ==> sats(A, satisfies_is_a_fm(u, x, y, z), env) <->
          satisfies_is_a(##A, nth(u, env), nth(x, env), nth(y, env), nth(z, env))

lemma satisfies_is_a_iff_sats:

      [| nth(u, env) = nu; nth(x, env) = nx; nth(y, env) = ny; nth(z, env) = nz;
         u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A) |]
      ==> satisfies_is_a(##A, nu, nx, ny, nz) <->
          sats(A, satisfies_is_a_fm(u, x, y, z), env)

theorem satisfies_is_a_reflection:

      REFLECTS [%x. satisfies_is_a(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_a(##Lset(i), f(x), g(x), h(x), g'(x))]

#### The Operator @{term satisfies_is_b}, Internalized

lemma satisfies_is_b_type:

      [| A ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
      ==> satisfies_is_b_fm(A, x, y, z) ∈ formula

lemma sats_satisfies_is_b_fm:

      [| u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A) |]
      ==> sats(A, satisfies_is_b_fm(u, x, y, z), env) <->
          satisfies_is_b(##A, nth(u, env), nth(x, env), nth(y, env), nth(z, env))

lemma satisfies_is_b_iff_sats:

      [| nth(u, env) = nu; nth(x, env) = nx; nth(y, env) = ny; nth(z, env) = nz;
         u ∈ nat; x < length(env); y < length(env); z ∈ nat; env ∈ list(A) |]
      ==> satisfies_is_b(##A, nu, nx, ny, nz) <->
          sats(A, satisfies_is_b_fm(u, x, y, z), env)

theorem satisfies_is_b_reflection:

      REFLECTS [%x. satisfies_is_b(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_b(##Lset(i), f(x), g(x), h(x), g'(x))]

#### The Operator @{term satisfies_is_c}, Internalized

lemma satisfies_is_c_type:

      [| A ∈ nat; h ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat |]
      ==> satisfies_is_c_fm(A, h, x, y, z) ∈ formula

lemma sats_satisfies_is_c_fm:

      [| u ∈ nat; v ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> sats(A, satisfies_is_c_fm(u, v, x, y, z), env) <->
          satisfies_is_c
           (##A, nth(u, env), nth(v, env), nth(x, env), nth(y, env), nth(z, env))

lemma satisfies_is_c_iff_sats:

      [| nth(u, env) = nu; nth(v, env) = nv; nth(x, env) = nx; nth(y, env) = ny;
         nth(z, env) = nz; u ∈ nat; v ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat;
         env ∈ list(A) |]
      ==> satisfies_is_c(##A, nu, nv, nx, ny, nz) <->
          sats(A, satisfies_is_c_fm(u, v, x, y, z), env)

theorem satisfies_is_c_reflection:

      REFLECTS [%x. satisfies_is_c(L, f(x), g(x), h(x), g'(x), h'(x)),
         %i x. satisfies_is_c(##Lset(i), f(x), g(x), h(x), g'(x), h'(x))]

#### The Operator @{term satisfies_is_d}, Internalized

lemma satisfies_is_d_type:

      [| A ∈ nat; h ∈ nat; x ∈ nat; z ∈ nat |]
      ==> satisfies_is_d_fm(A, h, x, z) ∈ formula

lemma sats_satisfies_is_d_fm:

      [| u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> sats(A, satisfies_is_d_fm(u, x, y, z), env) <->
          satisfies_is_d(##A, nth(u, env), nth(x, env), nth(y, env), nth(z, env))

lemma satisfies_is_d_iff_sats:

      [| nth(u, env) = nu; nth(x, env) = nx; nth(y, env) = ny; nth(z, env) = nz;
         u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> satisfies_is_d(##A, nu, nx, ny, nz) <->
          sats(A, satisfies_is_d_fm(u, x, y, z), env)

theorem satisfies_is_d_reflection:

      REFLECTS [%x. satisfies_is_d(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_d(##Lset(i), f(x), g(x), h(x), g'(x))]

#### The Operator @{term satisfies_MH}, Internalized

lemma satisfies_MH_type:

      [| A ∈ nat; u ∈ nat; x ∈ nat; z ∈ nat |]
      ==> satisfies_MH_fm(A, u, x, z) ∈ formula

lemma sats_satisfies_MH_fm:

      [| u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> sats(A, satisfies_MH_fm(u, x, y, z), env) <->
          satisfies_MH(##A, nth(u, env), nth(x, env), nth(y, env), nth(z, env))

lemma satisfies_MH_iff_sats:

      [| nth(u, env) = nu; nth(x, env) = nx; nth(y, env) = ny; nth(z, env) = nz;
         u ∈ nat; x ∈ nat; y ∈ nat; z ∈ nat; env ∈ list(A) |]
      ==> satisfies_MH(##A, nu, nx, ny, nz) <->
          sats(A, satisfies_MH_fm(u, x, y, z), env)

lemmas satisfies_reflections:

      (!!f g h.
          REFLECTS [%x. is_b(L, f(x), g(x), h(x)),
             %i x. is_b(##Lset(i), f(x), g(x), h(x))])
      ==> REFLECTS [%x. is_lambda(L, A(x), is_b(L, x), f(x)),
             %i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i), x), f(x))]

      REFLECTS [%x. is_formula(L, f(x)), %i x. is_formula(##Lset(i), f(x))]

      [| !!h f g g'.
            REFLECTS [%x. is_a(L, h(x), f(x), g(x), g'(x)),
               %i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_b(L, h(x), f(x), g(x), g'(x)),
               %i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_c(L, h(x), f(x), g(x), g'(x)),
               %i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_d(L, h(x), f(x), g(x)),
               %i x. is_d(##Lset(i), h(x), f(x), g(x))] |]
      ==> REFLECTS
             [%x. is_formula_case
                   (L, is_a(L, x), is_b(L, x), is_c(L, x), is_d(L, x), g(x), h(x)),
             %i x. is_formula_case
                    (##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x),
                     is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]

      REFLECTS [%x. satisfies_is_a(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_a(##Lset(i), f(x), g(x), h(x), g'(x))]

      REFLECTS [%x. satisfies_is_b(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_b(##Lset(i), f(x), g(x), h(x), g'(x))]

      REFLECTS [%x. satisfies_is_c(L, f(x), g(x), h(x), g'(x), h'(x)),
         %i x. satisfies_is_c(##Lset(i), f(x), g(x), h(x), g'(x), h'(x))]

      REFLECTS [%x. satisfies_is_d(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_d(##Lset(i), f(x), g(x), h(x), g'(x))]

lemmas satisfies_reflections:

      (!!f g h.
          REFLECTS [%x. is_b(L, f(x), g(x), h(x)),
             %i x. is_b(##Lset(i), f(x), g(x), h(x))])
      ==> REFLECTS [%x. is_lambda(L, A(x), is_b(L, x), f(x)),
             %i x. is_lambda(##Lset(i), A(x), is_b(##Lset(i), x), f(x))]

      REFLECTS [%x. is_formula(L, f(x)), %i x. is_formula(##Lset(i), f(x))]

      [| !!h f g g'.
            REFLECTS [%x. is_a(L, h(x), f(x), g(x), g'(x)),
               %i x. is_a(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_b(L, h(x), f(x), g(x), g'(x)),
               %i x. is_b(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_c(L, h(x), f(x), g(x), g'(x)),
               %i x. is_c(##Lset(i), h(x), f(x), g(x), g'(x))];
         !!h f g g'.
            REFLECTS [%x. is_d(L, h(x), f(x), g(x)),
               %i x. is_d(##Lset(i), h(x), f(x), g(x))] |]
      ==> REFLECTS
             [%x. is_formula_case
                   (L, is_a(L, x), is_b(L, x), is_c(L, x), is_d(L, x), g(x), h(x)),
             %i x. is_formula_case
                    (##Lset(i), is_a(##Lset(i), x), is_b(##Lset(i), x),
                     is_c(##Lset(i), x), is_d(##Lset(i), x), g(x), h(x))]

      REFLECTS [%x. satisfies_is_a(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_a(##Lset(i), f(x), g(x), h(x), g'(x))]

      REFLECTS [%x. satisfies_is_b(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_b(##Lset(i), f(x), g(x), h(x), g'(x))]

      REFLECTS [%x. satisfies_is_c(L, f(x), g(x), h(x), g'(x), h'(x)),
         %i x. satisfies_is_c(##Lset(i), f(x), g(x), h(x), g'(x), h'(x))]

      REFLECTS [%x. satisfies_is_d(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_is_d(##Lset(i), f(x), g(x), h(x), g'(x))]

theorem satisfies_MH_reflection:

      REFLECTS [%x. satisfies_MH(L, f(x), g(x), h(x), g'(x)),
         %i x. satisfies_MH(##Lset(i), f(x), g(x), h(x), g'(x))]

### Lemmas for Instantiating the Locale @{text "M_satisfies"}

#### The @{term "Member"} Case

lemma Member_Reflects:

      REFLECTS
         [%u. ∃v[L]. v ∈ B ∧
                     (∃bo[L].
                         ∃nx[L].
                            ∃ny[L].
                               v ∈ lstA ∧
                               is_nth(L, x, v, nx) ∧
                               is_nth(L, y, v, ny) ∧
                               is_bool_of_o(L, nx ∈ ny, bo) ∧ pair(L, v, bo, u)),
         %i u. ∃v∈Lset(i).
                  v ∈ B ∧
                  (∃bo∈Lset(i).
                      ∃nx∈Lset(i).
                         ∃ny∈Lset(i).
                            v ∈ lstA ∧
                            is_nth(##Lset(i), x, v, nx) ∧
                            is_nth(##Lset(i), y, v, ny) ∧
                            is_bool_of_o(##Lset(i), nx ∈ ny, bo) ∧
                            pair(##Lset(i), v, bo, u))]

lemma Member_replacement:

      [| L(A); x ∈ nat; y ∈ nat |]
      ==> strong_replacement
           (L, %env z.
                  ∃bo[L].
                     ∃nx[L].
                        ∃ny[L].
                           env ∈ list(A) ∧
                           is_nth(L, x, env, nx) ∧
                           is_nth(L, y, env, ny) ∧
                           is_bool_of_o(L, nx ∈ ny, bo) ∧ pair(L, env, bo, z))

#### The @{term "Equal"} Case

lemma Equal_Reflects:

      REFLECTS
         [%u. ∃v[L]. v ∈ B ∧
                     (∃bo[L].
                         ∃nx[L].
                            ∃ny[L].
                               v ∈ lstA ∧
                               is_nth(L, x, v, nx) ∧
                               is_nth(L, y, v, ny) ∧
                               is_bool_of_o(L, nx = ny, bo) ∧ pair(L, v, bo, u)),
         %i u. ∃v∈Lset(i).
                  v ∈ B ∧
                  (∃bo∈Lset(i).
                      ∃nx∈Lset(i).
                         ∃ny∈Lset(i).
                            v ∈ lstA ∧
                            is_nth(##Lset(i), x, v, nx) ∧
                            is_nth(##Lset(i), y, v, ny) ∧
                            is_bool_of_o(##Lset(i), nx = ny, bo) ∧
                            pair(##Lset(i), v, bo, u))]

lemma Equal_replacement:

      [| L(A); x ∈ nat; y ∈ nat |]
      ==> strong_replacement
           (L, %env z.
                  ∃bo[L].
                     ∃nx[L].
                        ∃ny[L].
                           env ∈ list(A) ∧
                           is_nth(L, x, env, nx) ∧
                           is_nth(L, y, env, ny) ∧
                           is_bool_of_o(L, nx = ny, bo) ∧ pair(L, env, bo, z))

#### The @{term "Nand"} Case

lemma Nand_Reflects:

      REFLECTS
         [%x. ∃u[L]. u ∈ B ∧
                     (∃rpe[L].
                         ∃rqe[L].
                            ∃andpq[L].
                               ∃notpq[L].
                                  fun_apply(L, rp, u, rpe) ∧
                                  fun_apply(L, rq, u, rqe) ∧
                                  is_and(L, rpe, rqe, andpq) ∧
                                  is_not(L, andpq, notpq) ∧
                                  u ∈ list(A) ∧ pair(L, u, notpq, x)),
         %i x. ∃u∈Lset(i).
                  u ∈ B ∧
                  (∃rpe∈Lset(i).
                      ∃rqe∈Lset(i).
                         ∃andpq∈Lset(i).
                            ∃notpq∈Lset(i).
                               fun_apply(##Lset(i), rp, u, rpe) ∧
                               fun_apply(##Lset(i), rq, u, rqe) ∧
                               is_and(##Lset(i), rpe, rqe, andpq) ∧
                               is_not(##Lset(i), andpq, notpq) ∧
                               u ∈ list(A) ∧ pair(##Lset(i), u, notpq, x))]

lemma Nand_replacement:

      [| L(A); L(rp); L(rq) |]
      ==> strong_replacement
           (L, %env z.
                  ∃rpe[L].
                     ∃rqe[L].
                        ∃andpq[L].
                           ∃notpq[L].
                              fun_apply(L, rp, env, rpe) ∧
                              fun_apply(L, rq, env, rqe) ∧
                              is_and(L, rpe, rqe, andpq) ∧
                              is_not(L, andpq, notpq) ∧
                              env ∈ list(A) ∧ pair(L, env, notpq, z))

#### The @{term "Forall"} Case

lemma Forall_Reflects:

      REFLECTS
         [%x. ∃u[L]. u ∈ B ∧
                     (∃bo[L].
                         u ∈ list(A) ∧
                         is_bool_of_o
                          (L, ∀a[L]. ∀co[L].
                                        ∀rpco[L].
                                           a ∈ A -->
                                           is_Cons(L, a, u, co) -->
                                           fun_apply(L, rp, co, rpco) -->
                                           number1(L, rpco),
                           bo) ∧
                         pair(L, u, bo, x)),
         %i x. ∃u∈Lset(i).
                  u ∈ B ∧
                  (∃bo∈Lset(i).
                      u ∈ list(A) ∧
                      is_bool_of_o
                       (##Lset(i),
                        ∀a∈Lset(i).
                           ∀co∈Lset(i).
                              ∀rpco∈Lset(i).
                                 a ∈ A -->
                                 is_Cons(##Lset(i), a, u, co) -->
                                 fun_apply(##Lset(i), rp, co, rpco) -->
                                 number1(##Lset(i), rpco),
                        bo) ∧
                      pair(##Lset(i), u, bo, x))]

lemma Forall_replacement:

      [| L(A); L(rp) |]
      ==> strong_replacement
           (L, %env z.
                  ∃bo[L].
                     env ∈ list(A) ∧
                     is_bool_of_o
                      (L, ∀a[L]. ∀co[L].
                                    ∀rpco[L].
                                       a ∈ A -->
                                       is_Cons(L, a, env, co) -->
                                       fun_apply(L, rp, co, rpco) -->
                                       number1(L, rpco),
                       bo) ∧
                     pair(L, env, bo, z))

#### The @{term "transrec_replacement"} Case

lemma formula_rec_replacement_Reflects:

      REFLECTS
         [%x. ∃u[L]. u ∈ B ∧
                     (∃y[L]. pair(L, u, y, x) ∧
                             is_wfrec(L, satisfies_MH(L, A), mesa, u, y)),
         %i x. ∃u∈Lset(i).
                  u ∈ B ∧
                  (∃y∈Lset(i).
                      pair(##Lset(i), u, y, x) ∧
                      is_wfrec(##Lset(i), satisfies_MH(##Lset(i), A), mesa, u, y))]

lemma formula_rec_replacement:

      [| n ∈ nat; L(A) |] ==> transrec_replacement(L, satisfies_MH(L, A), n)

#### The Lambda Replacement Case

lemma formula_rec_lambda_replacement_Reflects:

      REFLECTS
         [%x. ∃u[L]. u ∈ B ∧
                     mem_formula(L, u) ∧
                     (∃c[L]. is_formula_case
                              (L, satisfies_is_a(L, A), satisfies_is_b(L, A),
                               satisfies_is_c(L, A, g), satisfies_is_d(L, A, g), u,
                               c) ∧
                             pair(L, u, c, x)),
         %i x. ∃u∈Lset(i).
                  u ∈ B ∧
                  mem_formula(##Lset(i), u) ∧
                  (∃c∈Lset(i).
                      is_formula_case
                       (##Lset(i), satisfies_is_a(##Lset(i), A),
                        satisfies_is_b(##Lset(i), A), satisfies_is_c(##Lset(i), A, g),
                        satisfies_is_d(##Lset(i), A, g), u, c) ∧
                      pair(##Lset(i), u, c, x))]

lemma formula_rec_lambda_replacement:

      [| L(g); L(A) |]
      ==> strong_replacement
           (L, %x y. mem_formula(L, x) ∧
                     (∃c[L]. is_formula_case
                              (L, satisfies_is_a(L, A), satisfies_is_b(L, A),
                               satisfies_is_c(L, A, g), satisfies_is_d(L, A, g), x,
                               c) ∧
                             pair(L, x, c, y)))

### Instantiating @{text M_satisfies}

lemma M_satisfies_axioms_L:

      M_satisfies_axioms(L)

theorem M_satisfies_L:

      PROP M_satisfies(L)

lemmas satisfies_closed:

      [| L(A); p ∈ formula |] ==> L(satisfies(A, p))

and satisfies_abs:

      [| L(A); L(z); p ∈ formula |]
      ==> is_satisfies(L, A, p, z) <-> z = satisfies(A, p)

lemmas satisfies_closed:

      [| L(A); p ∈ formula |] ==> L(satisfies(A, p))

and satisfies_abs:

      [| L(A); L(z); p ∈ formula |]
      ==> is_satisfies(L, A, p, z) <-> z = satisfies(A, p)