---

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
  normalizes (using alternate method) to:
  
  λ%,a.
       (let ind(p,a,f,G) = case mFOLeffect(a)
                            of inl(x) =>
                            λs,%2. let %3,%4 = %2 
                                   in let a1,a2 = a 
                                      in let a3,a4 = a1 
                                         in let lbl,v1 = a2 
                                            in if lbl="andI"
                                                 then if mFOconnect?(a4)
                                                      then if mFOconnect-knd(a4)="and"
                                                           then λa,%4@0. <G 0 x[0] (%4 0) a %4@0
                                                                         , G 1 x[1] (%4 1) a %4@0
                                                                         >
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="impI"
                                                 then if mFOconnect?(a4)
                                                      then if mFOconnect-knd(a4)="imp"
                                                           then λa.if null(a3)
                                                                   then λx@0,y. (G 0 x[0] (%4 0) a y)
                                                                   else λx@0,y. (G 0 x[0] (%4 0) a <y, x@0>)
                                                                   fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="allI"
                                                 then if reduce(λh,p. ((¬bv1 ∈b mFOL-freevars(h))) ∧b p);inl Ax;a3)
                                                      then if v1 ∈b mFOL-freevars(a4)) then ⊥
                                                           if mFOquant?(a4)
                                                             then if (mFOquant-isall(a4) ∧b (inl Ax))
                                                                     ∨b((¬bmFOquant-isall(a4)) ∧b ff)
                                                                  then λa,%35,v. (G 0 x[0] (%4 0) 
                                                                                  (λz.if (z =z v1) then v else a z fi ) 
                                                                                  %35)
                                                                  else ⊥
                                                                  fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="existsI"
                                                 then if mFOquant?(a4)
                                                      then if (mFOquant-isall(a4) ∧b (inr Ax ))
                                                              ∨b((¬bmFOquant-isall(a4)) ∧b tt)
                                                           then λa,%1@0. <a v1, G 0 x[0] (%4 0) a %1@0>
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="orI"
                                                 then if mFOconnect?(a4)
                                                      then if mFOconnect-knd(a4)="or"
                                                           then if v1
                                                                then λa,%3. (inl (G 0 x[0] (%4 0) a %3))
                                                                else λa,%3. (inr (G 0 x[0] (%4 0) a %3) )
                                                                fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="hyp"
                                                 then if a4 ∈b a3)
                                                      then let x,%11 = rec-case(a3) of
                                                                       [] => λx.<λ%.⊥, λ%.Ax>
                                                                       a::L =>
                                                                        r.λx.<λ-any.if eq_mFO(a;x)
                                                                                    then <0, Ax, Ax>
                                                                                    else let %8,%9 = r x 
                                                                                         in let i,%4,%5 = %8 Ax in 
                                                                                            <i + 1, Ax, Ax>
                                                                                    fi 
                                                                             , λ-any.ifunion(eq_mFO(a;x); Ax)
                                                                             > 
                                                                       a4 
                                                           in let i,%11,%12 = x Ax in 
                                                              λa,x. x.i
                                                      else ⊥
                                                      fi 
                                               if lbl="andE"
                                                 then if v1 <z ||a3||
                                                      then if mFOconnect?(a3[v1])
                                                           then if mFOconnect-knd(a3[v1])="and"
                                                                then λa.if a3 = Ax then λ%4@0.(G 0 x[0] (%4 0) a 
                                                                                               <if v1 + 1 ≤z 0
                                                                                                then let %23,%24 =
                                                                                                      ⊥ a 
                                                                                                      let %24,%25 =
                                                                                                       %4@0.v1 
                                                                                                      in %25 
                                                                                                     in %23
                                                                                                else let %23,%24 =
                                                                                                      let %24,%25 =
                                                                                                       %4@0.v1 
                                                                                                      in %25.v1 + 1 
                                                                                                     in %23
                                                                                                fi 
                                                                                               , let %24,%25 = %4@0.v1 
                                                                                                 in %25
                                                                                               >)
                                                                        otherwise let u,v = a3 
                                                                                  in λ%4@0.(G 0 x[0] (%4 0) a 
                                                                                            <if v1 + 1 ≤z 0
                                                                                            then let %23,%24 =
                                                                                                  ⊥ a 
                                                                                                  <let %24,%25 =
                                                                                                    %4@0.v1 
                                                                                                   in %25
                                                                                                  , %4@0
                                                                                                  > 
                                                                                                 in %23
                                                                                            else let %23,%24 =
                                                                                                  <let %24,%25 =
                                                                                                    %4@0.v1 
                                                                                                   in %25
                                                                                                  , %4@0
                                                                                                  >.v1 + 1 
                                                                                                 in %23
                                                                                            fi 
                                                                                            , let %24,%25 = %4@0.v1 
                                                                                              in %25
                                                                                            , %4@0>)
                                                                else ⊥
                                                                fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="orE"
                                                 then if v1 <z ||a3||
                                                      then if mFOconnect?(a3[v1])
                                                           then if mFOconnect-knd(a3[v1])="or"
                                                                then λa,x@0. case x@0.v1
                                                                             of inl(a@0) =>
                                                                             G 0 x[0] (%4 0) a <a@0, x@0>
                                                                             | inr(b) =>
                                                                             G 1 x[1] (%4 1) a <b, x@0>
                                                                else ⊥
                                                                fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="impE"
                                                 then if v1 <z ||a3||
                                                      then if mFOconnect?(a3[v1])
                                                           then if mFOconnect-knd(a3[v1])="imp"
                                                                then λa.if a3 = Ax then λ%4@0.(G 1 x[1] (%4 1) a 
                                                                                               (%4@0.v1 
                                                                                                (G 0 x[0] (%4 0) a 
                                                                                                 %4@0)))
                                                                        otherwise let u,v = a3 
                                                                                  in λ%4@0.(G 1 x[1] (%4 1) a 
                                                                                            <%4@0.v1 
                                                                                             (G 0 x[0] (%4 0) a %4@0)
                                                                                            , %4@0
                                                                                            >)
                                                                else ⊥
                                                                fi 
                                                           else ⊥
                                                           fi 
                                                      else ⊥
                                                      fi 
                                               if lbl="allE"
                                                 then let hypnum,v2 = v1 
                                                      in if hypnum <z ||a3||
                                                         then if mFOquant?(a3[hypnum])
                                                              then if (mFOquant-isall(a3[hypnum]) ∧b (inl Ax))
                                                                      ∨b((¬bmFOquant-isall(a3[hypnum])) ∧b ff)
                                                                   then λa.if if if a3 = Ax then inl Ax
                                                                                 otherwise inr Ax 
                                                                              then inl Ax
                                                                              else inr Ax 
                                                                              fi 
                                                                           then λ%4@0.(G 0 x[0] (%4 0) a 
                                                                                       (%4@0.hypnum (a v2)))
                                                                           else let u,v = a3 
                                                                                in λ%4@0.(G 0 x[0] (%4 0) a 
                                                                                          <%4@0.hypnum (a v2), %4@0>)
                                                                           fi 
                                                                   else ⊥
                                                                   fi 
                                                              else ⊥
                                                              fi 
                                                         else ⊥
                                                         fi 
                                               if lbl="existsE"
                                                 then let hypnum,v2 = v1 
                                                      in if hypnum <z ||a3||
                                                         then if reduce(λh,p. ((¬bv2 ∈b mFOL-freevars(h))) ∧b p);...;...\000C)
                                                              then ...
                                                              else ...
                                                              fi 
                                                         else ...
                                                         fi 
                                               else ...
                                               fi 
                            | inr(x) =>
                            ... in 
        letrec F(p,w) = let a,f=w in 
                        ind(p,a,f,λb.F(...,f(b)) in 
        F(...;...) 
        ... 
        ... 
        ... 
        ...)
  
  not unfolding  ifunion listops boolops mFOLop pW-rec select-tuple le_int lt_int eq_int
  finishing with ... }

---

Latex:


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


By

Extract  of  Obid:  mFOL-proveable-formula-evidence
normalizes  (using  alternate  method)  to:

\mlambda{}\%,a.
          (let  ind(p,a,f,G)  =  case  mFOLeffect(a)
                                                    of  inl(x)  =>
                                                    \mlambda{}s,\%2.
                                                                let  \%3,\%4  =  \%2 
                                                                in  let  a1,a2  =  a 
                                                                      in  let  a3,a4  =  a1 
                                                                            in  let  lbl,v1  =  a2 
                                                                                  in  if  lbl="andI"
                                                                                            then  if  mFOconnect?(a4)
                                                                                                      then  if  mFOconnect-knd(a4)="and"
                                                                                                                then  \mlambda{}a,\%4@0.  <G  0  x[0]  (\%4  0)  a  \%4@0
                                                                                                                                            ,  G  1  x[1]  (\%4  1)  a  \%4@0
                                                                                                                                            >
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="impI"
                                                                                            then  if  mFOconnect?(a4)
                                                                                                      then  if  mFOconnect-knd(a4)="imp"
                                                                                                                then  \mlambda{}a.if  null(a3)
                                                                                                                                then  \mlambda{}x@0,y.  (G  0  x[0]  (\%4  0)  a  y)
                                                                                                                                else  \mlambda{}x@0,y.  (G  0  x[0]  (\%4  0)  a 
                                                                                                                                                            <y,  x@0>)
                                                                                                                                fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="allI"
                                                                                            then  if  reduce(\mlambda{}h,p.  ((\mneg{}\msubb{}v1  \mmember{}\msubb{}  mFOL-freevars(h)))
                                                                                                                                    \mwedge{}\msubb{}  p);inl  Ax;a3)
                                                                                                      then  if  v1  \mmember{}\msubb{}  mFOL-freevars(a4))  then  \mbot{}
                                                                                                                if  mFOquant?(a4)
                                                                                                                    then  if  (mFOquant-isall(a4)  \mwedge{}\msubb{}  (inl  Ax))
                                                                                                                                    \mvee{}\msubb{}((\mneg{}\msubb{}mFOquant-isall(a4))  \mwedge{}\msubb{}  ff)
                                                                                                                              then  \mlambda{}a,\%35,v.  (G  0  x[0]  (\%4  0) 
                                                                                                                                                              (\mlambda{}z.if  (z  =\msubz{}  v1)
                                                                                                                                                                      then  v
                                                                                                                                                                      else  a  z
                                                                                                                                                                      fi  ) 
                                                                                                                                                              \%35)
                                                                                                                              else  \mbot{}
                                                                                                                              fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="existsI"
                                                                                            then  if  mFOquant?(a4)
                                                                                                      then  if  (mFOquant-isall(a4)  \mwedge{}\msubb{}  (inr  Ax  ))
                                                                                                                      \mvee{}\msubb{}((\mneg{}\msubb{}mFOquant-isall(a4))  \mwedge{}\msubb{}  tt)
                                                                                                                then  \mlambda{}a,\%1@0.  <a  v1,  G  0  x[0]  (\%4  0)  a  \%1@0>
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="orI"
                                                                                            then  if  mFOconnect?(a4)
                                                                                                      then  if  mFOconnect-knd(a4)="or"
                                                                                                                then  if  v1
                                                                                                                          then  \mlambda{}a,\%3.  (inl  (G  0  x[0]  (\%4  0)  a 
                                                                                                                                                              \%3))
                                                                                                                          else  \mlambda{}a,\%3.  (inr  (G  0  x[0]  (\%4  0)  a 
                                                                                                                                                              \%3)  )
                                                                                                                          fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="hyp"
                                                                                            then  if  a4  \mmember{}\msubb{}  a3)
                                                                                                      then  let  x,\%11  =
                                                                                                                  rec-case(a3)  of
                                                                                                                  []  =>  \mlambda{}x.<\mlambda{}\%.\mbot{},  \mlambda{}\%.Ax>
                                                                                                                  a::L  =>
                                                                                                                    r.\mlambda{}x.<\mlambda{}-any.if  eq\_mFO(a;x)
                                                                                                                                            then  ɘ,  Ax,  Ax>
                                                                                                                                            else  let  \%8,\%9  =  r  x 
                                                                                                                                                      in  let  i,\%4,\%5  =  \%8 
                                                                                                                                                                                        Ax  in 
                                                                                                                                                            <i  +  1,  Ax,  Ax>
                                                                                                                                            fi 
                                                                                                                              ,  \mlambda{}-any.ifunion(eq\_mFO(a;x);  Ax)
                                                                                                                              > 
                                                                                                                  a4 
                                                                                                                in  let  i,\%11,\%12  =  x  Ax  in 
                                                                                                                      \mlambda{}a,x.  x.i
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="andE"
                                                                                            then  if  v1  <z  ||a3||
                                                                                                      then  if  mFOconnect?(a3[v1])
                                                                                                                then  if  mFOconnect-knd(a3[v1])="and"
                                                                                                                          then  \mlambda{}a.if  a3  =  Ax
                                                                                                                                          then  \mlambda{}\%4@0.(G  0  x[0]  (\%4  0)  a 
                                                                                                                                                                  <if  v1  +  1  \mleq{}z  0
                                                                                                                                                                    then  let  \%23,\%24  =
                                                                                                                                                                                \mbot{}  a 
                                                                                                                                                                                ... 
                                                                                                                                                                              in  \%23
                                                                                                                                                                    else  let  \%23,\%24  =
                                                                                                                                                                                ....v1  +  1 
                                                                                                                                                                              in  \%23
                                                                                                                                                                    fi 
                                                                                                                                                                  ,  let  \%24,\%25  =
                                                                                                                                                                        \%4@0.v1 
                                                                                                                                                                      in  \%25
                                                                                                                                                                  >)
                                                                                                                                          otherwise  let  u,v  =  a3 
                                                                                                                                                              in  \mlambda{}\%4@0.(G  0  x[0] 
                                                                                                                                                                                  (\%4  0) 
                                                                                                                                                                                  a 
                                                                                                                                                                                  <if  ...
                                                                                                                                                                                  then  ...
                                                                                                                                                                                  else  ...
                                                                                                                                                                                  fi 
                                                                                                                                                                                  ,  ...
                                                                                                                                                                                  ,  \%4@0>)
                                                                                                                          else  \mbot{}
                                                                                                                          fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="orE"
                                                                                            then  if  v1  <z  ||a3||
                                                                                                      then  if  mFOconnect?(a3[v1])
                                                                                                                then  if  mFOconnect-knd(a3[v1])="or"
                                                                                                                          then  \mlambda{}a,x@0.  case  x@0.v1
                                                                                                                                                    of  inl(a@0)  =>
                                                                                                                                                    G  0  x[0]  (\%4  0)  a 
                                                                                                                                                    <a@0,  x@0>
                                                                                                                                                    |  inr(b)  =>
                                                                                                                                                    G  1  x[1]  (\%4  1)  a  <b,  x@0>
                                                                                                                          else  \mbot{}
                                                                                                                          fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="impE"
                                                                                            then  if  v1  <z  ||a3||
                                                                                                      then  if  mFOconnect?(a3[v1])
                                                                                                                then  if  mFOconnect-knd(a3[v1])="imp"
                                                                                                                          then  \mlambda{}a.if  a3  =  Ax
                                                                                                                                          then  \mlambda{}\%4@0.(G  1  x[1]  (\%4  1)  a 
                                                                                                                                                                  (\%4@0.v1 
                                                                                                                                                                    (G  0  x[0]  (\%4  0) 
                                                                                                                                                                      a 
                                                                                                                                                                      \%4@0)))
                                                                                                                                          otherwise  let  u,v  =  a3 
                                                                                                                                                              in  \mlambda{}\%4@0.(G  1  x[1] 
                                                                                                                                                                                  (\%4  1) 
                                                                                                                                                                                  a 
                                                                                                                                                                                  <\%4@0.v1 
                                                                                                                                                                                    (G  0  x[0] 
                                                                                                                                                                                      (\%4  0) 
                                                                                                                                                                                      a 
                                                                                                                                                                                      \%4@0)
                                                                                                                                                                                  ,  \%4@0
                                                                                                                                                                                  >)
                                                                                                                          else  \mbot{}
                                                                                                                          fi 
                                                                                                                else  \mbot{}
                                                                                                                fi 
                                                                                                      else  \mbot{}
                                                                                                      fi 
                                                                                        if  lbl="allE"
                                                                                            then  let  hypnum,v2  =  v1 
                                                                                                      in  if  hypnum  <z  ||a3||
                                                                                                            then  if  mFOquant?(a3[hypnum])
                                                                                                                      then  if  (mFOquant-isall(a3[hypnum])
                                                                                                                                      \mwedge{}\msubb{}  (inl  Ax))
                                                                                                                                      \mvee{}\msubb{}((\mneg{}\msubb{}mFOquant-isall(a3[hypnum]))
                                                                                                                                          \mwedge{}\msubb{}  ff)
                                                                                                                                then  \mlambda{}a.if  if  if  a3  =  Ax  then  inl  Ax
                                                                                                                                                            otherwise  inr  Ax 
                                                                                                                                                      then  inl  Ax
                                                                                                                                                      else  inr  Ax 
                                                                                                                                                      fi 
                                                                                                                                                then  \mlambda{}\%4@0.(G  0  x[0]  (\%4  0) 
                                                                                                                                                                        a 
                                                                                                                                                                        (\%4@0.hypnum 
                                                                                                                                                                          (a  v2)))
                                                                                                                                                else  let  u,v  =  a3 
                                                                                                                                                          in  \mlambda{}\%4@0.(G  0  x[0] 
                                                                                                                                                                              (\%4  0) 
                                                                                                                                                                              a 
                                                                                                                                                                              <\%4@0.hypnum 
                                                                                                                                                                                (a  v2)
                                                                                                                                                                              ,  \%4@0
                                                                                                                                                                              >)
                                                                                                                                                fi 
                                                                                                                                else  \mbot{}
                                                                                                                                fi 
                                                                                                                      else  \mbot{}
                                                                                                                      fi 
                                                                                                            else  \mbot{}
                                                                                                            fi 
                                                                                        if  lbl="existsE"
                                                                                            then  let  hypnum,v2  =  v1 
                                                                                                      in  if  hypnum  <z  ||a3||
                                                                                                            then  if  reduce(\mlambda{}h,p.  ((\mneg{}\msubb{}v2  \mmember{}\msubb{} 
                                                                                                                                                                  mFOL-freevars(h)))
                                                                                                                                                    \mwedge{}\msubb{}  p);inl  Ax;a3)
                                                                                                                      then  if  v2  \mmember{}\msubb{}  mFOL-freevars(a4))
                                                                                                                                    then  \mlambda{}\%.\mbot{}
                                                                                                                                if  if  v2  \mmember{}\msubb{}  mFOL-freevars(a4))
                                                                                                                                      then  inl  Ax
                                                                                                                                      else  inr  Ax 
                                                                                                                                      fi 
                                                                                                                                    then  \mbot{}
                                                                                                                                if  mFOquant?(a3[hypnum])
                                                                                                                                    then  if  (mFOquant-isall(a3[...])
                                                                                                                                                    \mwedge{}\msubb{}  (inr  Ax  ))
                                                                                                                                                    \mvee{}\msubb{}((\mneg{}\msubb{}mFOquant-isall(...))
                                                                                                                                                        \mwedge{}\msubb{}  tt)
                                                                                                                                                  then  \mlambda{}\%,a,\%.  let  d,\%44  =
                                                                                                                                                                              \%.hypnum 
                                                                                                                                                                            in  G  0  x[...] 
                                                                                                                                                                                  ... 
                                                                                                                                                                                  ... 
                                                                                                                                                                                  ...
                                                                                                                                              ...
                                                                                                                                ... 
                                                                                                                                ...
                                                                                                                      else  ...
                                                                                                                      fi 
                                                                                                            else  ...
                                                                                                            fi 
                                                                                        else  ...
                                                                                        fi 
                                                    |  inr(x)  =>
                                                    ...  in 
            letrec  F(p,w)  =  let  a,f=w  in 
                                            ind(p,a,f,\mlambda{}b.F(...,f(b))  in 
            F(...;...) 
            ... 
            ... 
            ... 
            ...)

not  unfolding    ifunion  listops  boolops  mFOLop  pW-rec  select-tuple  le\_int  lt\_int  eq\_int
finishing  with  ...

---

Home Index