---

Step * 1 1 1 1 1 of Lemma mFOL-evidence-value-type


1. fmla : mFOL()
⊢ mFOL_ind(fmla;
           mFOatomic(R,vars)⇒ ⋅;
           mFOconnect(knd,a,b)⇒ r1,r2.if knd =a "and" then <r1, r2>
           if knd =a "or" then inl r1
           else λx.r2
           fi ;
           mFOquant(isall,x,body)⇒ r.if isall then λx.r else <⋅, r> fi )  ∈ mFOL-abstract(fmla) Unit (λn,L. True) (λz.⋅\000C)
BY
{ xxx(SimpleDatatypeInduction 1 THEN Reduce 0 THEN RepUR ``mFOL-abstract`` 0 THEN Try (Fold `mFOL-abstract` 0))xxx }

1
1. sz : ℕ
2. ∀sz:ℕsz. ∀fmla:mFOL().
     mFOL_ind(fmla;
              mFOatomic(R,vars)⇒ ⋅;
              mFOconnect(knd,a,b)⇒ r1,r2.if knd =a "and" then <r1, r2>
              if knd =a "or" then inl r1
              else λx.r2
              fi ;
              mFOquant(isall,x,body)⇒ r.if isall then λx.r else <⋅, r> fi )  ∈ mFOL-abstract(fmla) Unit (λn,L. True) 
                                                                                (λz.⋅) 
     supposing mFOL_size(fmla) ≤ sz
3. name : Atom
4. f2 : ℤ List
5. 0 ≤ sz
⊢ ⋅ ∈ AbstractFOAtomic(name;f2) Unit (λn,L. True) (λz.⋅)

2
1. knd : Atom
2. left : mFOL()
3. f3 : mFOL()
4. mFOL_ind(f3;
            mFOatomic(R,vars)⇒ ⋅;
            mFOconnect(knd,a,b)⇒ r1,r2.if knd =a "and" then <r1, r2>
            if knd =a "or" then inl r1
            else λx.r2
            fi ;
            mFOquant(isall,x,body)⇒ r.if isall then λx.r else <⋅, r> fi )  ∈ mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅)
5. mFOL_ind(left;
            mFOatomic(R,vars)⇒ ⋅;
            mFOconnect(knd,a,b)⇒ r1,r2.if knd =a "and" then <r1, r2>
            if knd =a "or" then inl r1
            else λx.r2
            fi ;
            mFOquant(isall,x,body)⇒ r.if isall then λx.r else <⋅, r> fi )  ∈ mFOL-abstract(left) Unit (λn,L. True) (λz.\000C⋅)
⊢ if knd =a "and"
    then <mFOL_ind(left;
                   mFOatomic(name,vars)⇒ ⋅;
                   mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                   if knd =a "or" then inl rec1
                   else λx.rec2
                   fi ;
                   mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
         , mFOL_ind(f3;
                    mFOatomic(name,vars)⇒ ⋅;
                    mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                    if knd =a "or" then inl rec1
                    else λx.rec2
                    fi ;
                    mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
         >
  if knd =a "or"
    then inl mFOL_ind(left;
                      mFOatomic(name,vars)⇒ ⋅;
                      mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                      if knd =a "or" then inl rec1
                      else λx.rec2
                      fi ;
                      mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
  else λx.mFOL_ind(f3;
                   mFOatomic(name,vars)⇒ ⋅;
                   mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                   if knd =a "or" then inl rec1
                   else λx.rec2
                   fi ;
                   mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
  fi  ∈ FOConnective(knd) mFOL-abstract(left) mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅)

3
1. isall : 𝔹
2. var : ℤ
3. f3 : mFOL()
4. mFOL_ind(f3;
            mFOatomic(R,vars)⇒ ⋅;
            mFOconnect(knd,a,b)⇒ r1,r2.if knd =a "and" then <r1, r2>
            if knd =a "or" then inl r1
            else λx.r2
            fi ;
            mFOquant(isall,x,body)⇒ r.if isall then λx.r else <⋅, r> fi )  ∈ mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅)
⊢ if isall
  then λx.mFOL_ind(f3;
                   mFOatomic(name,vars)⇒ ⋅;
                   mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                   if knd =a "or" then inl rec1
                   else λx.rec2
                   fi ;
                   mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
  else <⋅
       , mFOL_ind(f3;
                  mFOatomic(name,vars)⇒ ⋅;
                  mFOconnect(knd,left,right)⇒ rec1,rec2.if knd =a "and" then <rec1, rec2>
                  if knd =a "or" then inl rec1
                  else λx.rec2
                  fi ;
                  mFOquant(isall,var,body)⇒ rec3.if isall then λx.rec3 else <⋅, rec3> fi ) 
       >
  fi  ∈ FOQuantifier(isall) var mFOL-abstract(f3) Unit (λn,L. True) (λz.⋅)

---

Latex:

---

Latex:

1.  fmla  :  mFOL()
\mvdash{}  mFOL\_ind(fmla;
                      mFOatomic(R,vars){}\mRightarrow{}  \mcdot{};
                      mFOconnect(knd,a,b){}\mRightarrow{}  r1,r2.if  knd  =a  "and"  then  <r1,  r2>
                      if  knd  =a  "or"  then  inl  r1
                      else  \mlambda{}x.r2
                      fi  ;
                      mFOquant(isall,x,body){}\mRightarrow{}  r.if  isall  then  \mlambda{}x.r  else  <\mcdot{},  r>  fi  )    \mmember{}  mFOL-abstract(fmla) 
                                                                                                                                                          Unit 
                                                                                                                                                          (\mlambda{}n,L.  True) 
                                                                                                                                                          (\mlambda{}z.\mcdot{})


By

---

Latex:
xxx(SimpleDatatypeInduction  1
        THEN  Reduce  0
        THEN  RepUR  ``mFOL-abstract``  0
        THEN  Try  (Fold  `mFOL-abstract`  0))xxx

---

Home Index