---

Step * of Lemma mFOL-proveable-formula-evidence-ext

∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
BY
{ Extract of Obid: mFOL-proveable-formula-evidence
  not unfolding  proof_tree_ind listops boolops mFOLop select-tuple le_int lt_int eq_int 
  finishing with Auto
  unfolds to:
  
  λ%,a.
       (proof_tree_ind(λsr.mFOLeffect(sr);λs,r,s@0,%1@0.
                                                        (case mFOLeffect(<s, r>)
                                                          of inl(x) =>
                                                          λ%1,s@0,%2. Ax
                                                          | inr(y) =>
                                                          λ%1,s@0,%2. let %3,%4 = %2 in Ax 
                                                         Ax 
                                                         s@0 
                                                         %1@0);λs,r,L,%2,s@0,%3.
                                                                   (case mFOLeffect(<s, r>)
                                                                     of inl(x) =>
                                                                     λ%1,L,%2,%3,s@0,%4.
                                                                                        let %5,%6 = %4 
                                                                                        in let s1,s2 = s 
                                                                                           in let lbl,v1 = r 
                                                                                              in if lbl="andI"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="impI"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="allI"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="existsI"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="orI"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="orI"
                                                                                                   then Ax
                                                                                                 if lbl="hyp"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="andE"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="orE"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="impE"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="allE"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 if lbl="existsE"
                                                                                                   then λ%.(... 
                                                                                                            Ax)
                                                                                                 else λ%.Ax
                                                                                                 fi  
                                                                                              Ax
                                                                     | inr(y) =>
                                                                     λ%1,L,%2,%3,s@0,%4. Ax 
                                                                    Ax 
                                                                    L 
                                                                    Ax 
                                                                    %2 
                                                                    s@0 
                                                                    %3);%) 
        let x,y = let x,y = % 
                  in x 
        in x 
        (fix((λcorrect_proof,pf. let sr,f = pf 
                                 in <Ax
                                    , case mFOLeffect(sr) of inl(subgoals) => λi.(correct_proof (f i)) | inr(x) => Ax
                                    >)) 
         %) 
        a 
        Ax)
   }

---

Latex:

---

Latex:
\mforall{}[fmla:mFOL()].  (mFOL-proveable-formula(fmla)  {}\mRightarrow{}  mFOL-evidence(fmla))


By

---

Latex:
Extract  of  Obid:  mFOL-proveable-formula-evidence
not  unfolding    proof\_tree\_ind  listops  boolops  mFOLop  select-tuple  le\_int  lt\_int  eq\_int 
finishing  with  Auto
unfolds  to:

\mlambda{}\%,a.
          (proof\_tree\_ind(\mlambda{}sr.mFOLeffect(sr);\mlambda{}s,r,s@0,\%1@0.
                                                                                                            (case  mFOLeffect(<s,  r>)
                                                                                                                of  inl(x)  =>
                                                                                                                \mlambda{}\%1,s@0,\%2.  Ax
                                                                                                                |  inr(y)  =>
                                                                                                                \mlambda{}\%1,s@0,\%2.  let  \%3,\%4  =  \%2  in  Ax 
                                                                                                              Ax 
                                                                                                              s@0 
                                                                                                              \%1@0);\mlambda{}s,r,L,\%2,s@0,\%3.
                                                                                                                                  (case  mFOLeffect(<s,  r>)
                                                                                                                                      of  inl(x)  =>
                                                                                                                                      \mlambda{}\%1,L,\%2,\%3,s@0,\%4.  let  \%5,\%6  =
                                                                                                                                                                                \%4 
                                                                                                                                                                              in  ...
                                                                                                                                      |  inr(y)  =>
                                                                                                                                      \mlambda{}\%1,L,\%2,\%3,s@0,\%4.  Ax 
                                                                                                                                    Ax 
                                                                                                                                    L 
                                                                                                                                    Ax 
                                                                                                                                    \%2 
                                                                                                                                    s@0 
                                                                                                                                    \%3);\%) 
            let  x,y  =  let  x,y  =  \% 
                                in  x 
            in  x 
            (fix((\mlambda{}correct$_{proof}$,pf.  let  sr,f  =  pf 
                                                            in  <Ax
                                                                  ,  case  mFOLeffect(sr)
                                                                        of  inl(subgoals)  =>
                                                                        \mlambda{}i.(correct$_{proof}$  (f  i))
                                                                        |  inr(x)  =>
                                                                        Ax
                                                                  >)) 
              \%) 
            a 
            Ax)

---

Home Index