---

Step * of Lemma test-evd1'

∀[A,B,C,D,E:ℙ].  ((((A ∧ B) ⇒ (A ∧ B)) ⇒ (C ∨ D)) ⇒ (C ⇒ E) ⇒ (D ⇒ E) ⇒ E)
BY
{ (EvidenceTac ⌜λh,f,g. let I1 = λx.x^gcd(10;15) in
                         let I2 = λp.<fst(p), snd(p)>^hd(factorization(111)) in
                         if isl(h I1) then f else g fi  let x = h I2 in if isl(x) then outl(x) else outr(x) fi ⌝⋅
   THENA Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[A,B,C,D,E:\mBbbP{}].    ((((A  \mwedge{}  B)  {}\mRightarrow{}  (A  \mwedge{}  B))  {}\mRightarrow{}  (C  \mvee{}  D))  {}\mRightarrow{}  (C  {}\mRightarrow{}  E)  {}\mRightarrow{}  (D  {}\mRightarrow{}  E)  {}\mRightarrow{}  E)


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}h,f,g.  let  I1  =  \mlambda{}x.x\^{}gcd(10;15)  in
                                              let  I2  =  \mlambda{}p.<fst(p),  snd(p)>\^{}hd(factorization(111))  in
                                              if  isl(h  I1)  then  f  else  g  fi   
                                              let  x  =  h  I2  in
                                                      if  isl(x)  then  outl(x)  else  outr(x)  fi  \mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index