Proof of Nuprl Lemma : mFOL-proveable-formula-evidence-ext3

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

∀[fmla:mFOL()]. (mFOL-proveable-formula(fmla) ⇒ mFOL-evidence(fmla))
BY
{ Extract of Obid: mFOL-proveable-formula-evidence-ext2
  not unfolding  proof_tree_ind deq-member boolops ifunion mFOLop listops
  finishing with Auto
  normalizes to:

  λ%,a.
       (proof_tree_ind(λsr.mFOLeffect(sr);λs,r,s@0,%1@0. if mFOLeffect(<s, r>)
                                                        then Ax

                                                        else let %3,%4 = %1@0

                                                             in Ax

                                                        fi ;λs,r,L,%2,s@0,%3. case mFOLeffect(<s, r>)

                                                                 of inl(x) =>

                                                                 let %5,%6 = %3

                                                                 in let s1,s2 = s

                                                                    in let lbl,v1 = r

                                                                       in if lbl="andI"

                                                                            then if mFOconnect?(s2)

                                                                                 then if mFOconnect-knd(s2)="and"

                                                                                      then λa,%5. <%2 0 x[0] (%6 0) a %5

                                                                                                  , %2 1 x[1] (%6 1) a

%5

                                                                                      else Ax

fi

                                                                                 else Ax

fi

                                                                          if lbl="impI"

                                                                            then if mFOconnect?(s2)

                                                                                 then if mFOconnect-knd(s2)="imp"

                                                                                      then λa.if null(s1)

                                                                                              then λx@0,y. (%2 0 x[0]

                                                                                                            (%6 0)

y)

                                                                                              else λx@0,y. (%2 0 x[0]

                                                                                                            (%6 0)

                                                                                                            <y, x@0>)

fi

                                                                                      else Ax

fi

                                                                                 else Ax

fi

                                                                          if lbl="allI"

                                                                            then if v1 ∈_b

                                                                                      reduce(...;mFOL-freevars(s2);s1)

                                                                                   then Ax

                                                                                 if mFOquant?(s2)

                                                                                   then if if mFOquant-isall(s2)

                                                                                           then inl Ax

                                                                                           else inr Ax

fi

                                                                                           ∨_bifunion(mFOquant-isall(s2);

                                                                                                     inr Ax )

                                                                                        then let x1,%34 =

                                                                                              rec-case(s1) of

                                                                                              [] => λ-any.<λ-1.<-1

                                                                                                               , λi.Ax

                                                                                                          , λ-1,%1. Ax

                                                                                              a::L =>

                                                                                               r.λ-any.let x,%4 = r

                                                                                                                  -any

                                                                                                       in <λ-1.<λ%6.Ax

                                                                                                               , λi....

                                                                                                          , λ-1,-2. Ax

                                                                                              mFOL-freevars(s2)

                                                                                             in let %33,%34 = x1

                                                                                                              (λ%.Ax)

                                                                                                in λa,%36,v.

                                                                                                            (%2 0 x[0]

                                                                                                             (%6 0)

                                                                                                             (λz....)

                                                                                                             %36)

                                                                                        else Ax

fi

                                                                                 else Ax

fi

                                                                          if lbl="existsI"

                                                                            then if v1 ∈_b

                                                                                      reduce(...;mFOL-freevars(s2);s1)

                                                                                 then if mFOquant?(s2)

                                                                                      then if ifunion

                                                                                                (mFOquant-isall(s2);

                                                                                                 inr Ax )

                                                                                              ∨_bif mFOquant-isall(s2)

                                                                                                then inr Ax

                                                                                                else inl Ax

fi

                                                                                           then λa,%27. <a v1

                                                                                                        , %2 0 x[0]

                                                                                                          (%6 0)

%27

                                                                                           else Ax

fi

                                                                                      else Ax

fi

                                                                                 else Ax

fi

                                                                          if lbl="orI"

                                                                            then if mFOconnect?(s2)

                                                                                 then if mFOconnect-knd(s2)="or"

                                                                                      then if v1

                                                                                           then λa,%4. (inl (%2 0 x[0]

                                                                                                             (%6 0)

                                                                                                             %4))

                                                                                           else λa,%4. (inr (%2 0 x[0]

                                                                                                             (%6 0)

                                                                                                             %4) )

fi

                                                                                      else Ax

fi

                                                                                 else Ax

fi

                                                                          if lbl="orI"

                                                                            then Ax Ax

                                                                          if lbl="hyp"

                                                                            then if s2 ∈_b s1

                                                                                 then let x,y =

                                                                                       rec-case(s1) of

                                                                                       [] => λx.<λ%.Ax, λ%.Ax>

                                                                                       a::L =>

                                                                                        r.λx.<λ-any.if eq_mFO(a;x)

                                                                                                    then <0, Ax, Ax>

                                                                                                    else let %8,%9 = r

                                                                                                         in ...

fi

                                                                                             , λ-any.ifunion

                                                                                                       (eq_mFO(a;x); Ax)

s2

                                                                                      in let i,%14,%15 = x Ax in

                                                                                         λa,x. (...

i)

                                                                                 else Ax

fi

                                                                          if lbl="andE"

                                                                            then if (v1) < (||s1||)

                                                                                    then if mFOconnect?(s1[v1])

                                                                                         then if mFOconnect-knd(...)=...

                                                                                              then λa,%5.

                                                                                                         (%2 0 x[0]

                                                                                                          (%6 0)

                                                                                                          <if (0) < (v1

                                                                                                             + 1)

                                                                                                              then ...

                                                                                                              else ...

                                                                                                          , if null(s1)

                                                                                                            then ...

                                                                                                            else <...

                                                                                                                 , %5

fi

>)

                                                                                              else Ax

fi

                                                                                         else Ax

fi

                                                                                    else Ax

                                                                          if lbl="orE"

                                                                            then if (v1) < (||s1||)

                                                                                    then if mFOconnect?(s1[v1])

                                                                                         then if mFOconnect-knd(...)=...

                                                                                              then λa,x@0. ...

                                                                                              else Ax

fi

                                                                                         else Ax

fi

                                                                                    else Ax

                                                                          if lbl="impE"

                                                                            then if (v1) < (||s1||)

                                                                                    then if mFOconnect?(s1[v1])

                                                                                         then if mFOconnect-knd(...)=...

                                                                                              then λa,%5.

                                                                                                         (%2 1 x[1]

                                                                                                          (%6 1)

                                                                                                          if null(s1)

                                                                                                          then ...

%5

v1

                                                                                                               (%2 0

                                                                                                                x[0]

                                                                                                                (%6 0)

%5)

                                                                                                          else <...

%5

v1

                                                                                                                (%2 0

                                                                                                                 x[0]

                                                                                                                 (%6 0)

%5)

                                                                                                               , %5

                                                                                                          fi )

                                                                                              else Ax

fi

                                                                                         else Ax

fi

                                                                                    else Ax

                                                                          if lbl="allE"

                                                                            then let x1,y = v1

                                                                                 in if (x1) < (||s1||)

                                                                                       then if y ∈_b

                                                                                                 reduce(λh,vs. ...;...;s\000C1)

                                                                                            then if mFOquant?(s1[x1])

                                                                                                 then if if ...

                                                                                                         then inl Ax

                                                                                                         else inr Ax

fi

                                                                                                         ∨_bifunion

                                                                                                             (...;

                                                                                                              inr Ax )

                                                                                                      then ifunion

                                                                                                             (...;

                                                                                                              λa,...)

                                                                                                      else Ax

fi

                                                                                                 else Ax

fi

                                                                                            else Ax

fi

                                                                                       else Ax

                                                                          if lbl="existsE"

                                                                            then let x1,y = v1

                                                                                 in if (x1) < (||s1||)

                                                                                       then if y ∈_b

                                                                                                 reduce(λh,vs. ...;...;s\000C1)

                                                                                              then Ax

                                                                                            if mFOquant?(s1[x1])

                                                                                              then if ifunion

                                                                                                        (...;

                                                                                                         inr Ax )

                                                                                                      ∨_bif ...

                                                                                                        then inr Ax

                                                                                                        else inl Ax

fi

                                                                                                   then λa,%. ...

                                                                                                   else Ax

fi

                                                                                            else Ax

fi

                                                                                       else Ax

                                                                          else Ax

fi

                                                                 | inr(x) =>

                                                                 Ax;%)

        let x,y = %
        in fst(x)
        letrec correct_proof(pf)=let sr,f = pf

                                 in <Ax, if mFOLeffect(sr) then λi.(correct_proof (f i)) else Ax fi > in

         correct_proof(%)
        a
        Ax) }

Latex:

Latex:
\mforall{}[fmla:mFOL()]. (mFOL-proveable-formula(fmla) {}\mRightarrow{} mFOL-evidence(fmla)) By Latex: Extract of Obid: mFOL-proveable-formula-evidence-ext2 not unfolding proof\_tree\_ind deq-member boolops ifunion mFOLop listops finishing with Auto normalizes to: \mlambda{}\%,a. (proof\_tree\_ind(\mlambda{}sr.mFOLeffect(sr);\mlambda{}s,r,s@0,\%1@0. if mFOLeffect(<s, r>) then Ax else let \%3,\%4 = \%1@0 in Ax fi ;\mlambda{}s,r,L,\%2,s@0,\%3. case mFOLeffect(<s, r>) of inl(x) => let \%5,\%6 = \%3 in let s1,s2 = s in let lbl,v1 = r in if lbl="andI" then if mFOconnect?(s2) then if ...="and" then \mlambda{}a,\%5. ... else Ax fi else Ax fi if lbl="impI" then if mFOconnect?(s2) then if ...="imp" then \mlambda{}a.if ... then ... else ... fi else Ax fi else Ax fi if lbl="allI" then if v1 \mmember{}\msubb{} ... then Ax if mFOquant?(s2) then if if ... then inl Ax else ... fi \mvee{}\msubb{}ifunion (...; ...) then ... else Ax fi else Ax fi if lbl="existsI" then if v1 \mmember{}\msubb{} ... then if mFOquant?(s2) then if ifunion (...; ...) \mvee{}\msubb{}... then \mlambda{}a,... else Ax fi else Ax fi else Ax fi if lbl="orI" then if mFOconnect?(s2) then if ...="or" then if v1 then \mlambda{}a,... else \mlambda{}a,... fi else Ax fi else Ax fi if lbl="orI" then Ax Ax if lbl="hyp" then if s2 \mmember{}\msubb{} s1 then let x,y = rec-case(s1) of [] => \mlambda{}x.<\mlambda{}\%.Ax , ... > a::L => r.\mlambda{}x.<... , ... > s2 in ... else Ax fi if lbl="andE" then if (v1) < (||s1||) then if ... then ... else Ax fi else Ax if lbl="orE" then if (v1) < (||s1||) then if ... then ... else Ax fi else Ax if lbl="impE" then if (v1) < (||s1||) then if ... then ... else Ax fi else Ax if lbl="allE" then let x1,y = v1 in if (x1) < (||s1||) then if y \mmember{}\msubb{} ... then ... else Ax fi else Ax if lbl="existsE" then let x1,y = v1 in if (x1) < (||s1||) then if y \mmember{}\msubb{} ... then Ax if ... then ... else Ax fi else Ax else Ax fi | inr(x) => Ax;\%) let x,y = \% in fst(x) letrec correct$_{proof}$(pf)=let sr,f = pf in <Ax, if mFOLeffect(sr) then \mlambda{}i.(correct$_{proof}\mbackslash{}ff\000C24 (f i)) else Ax fi > in correct$_{proof}$(\%) a Ax) Home Index