---

Step * of Lemma test-model

∀[Dom:Type]. ∀[A,B:Dom ⟶ ℙ]. ∀[R:Dom ⟶ Dom ⟶ ℙ].
  ((∀x:Dom. ∃y:Dom. (R[x;y] ∧ (A[y] ∨ B[y])))
  ⇒ (∀x,y,z:Dom.  ((R[x;y] ∧ R[x;z] ∧ A[y] ∧ A[z]) ⇒ A[x]))
  ⇒ (∀x,y,z:Dom.  ((R[x;y] ∧ R[x;z] ∧ B[y] ∧ B[z]) ⇒ A[x]))
  ⇒ (∀x:Dom. A[x]))
BY
{ (EvidenceTac ⌜λf,g,h,x. let y,RAorB = f x 
                          in let R,AorB = RAorB 
                             in case AorB
                                 of inl(A) =>
                                 (λk.let y1,raORb = k x 
                                     in let r,aORb = raORb 
                                        in case aORb of inl(a) => g x y y1 <R, r, A, a> | inr(b) => Ax) 
                                 f
                                 | inr(B) =>
                                 (λk.let y1,raORb = k x 
                                     in let r,aORb = raORb 
                                        in case aORb of inl(a) => Ax | inr(b) => h x y y1 <R, r, B, b>) 
                                 f⌝⋅
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[Dom:Type].  \mforall{}[A,B:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Dom.  \mexists{}y:Dom.  (R[x;y]  \mwedge{}  (A[y]  \mvee{}  B[y])))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((R[x;y]  \mwedge{}  R[x;z]  \mwedge{}  A[y]  \mwedge{}  A[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    ((R[x;y]  \mwedge{}  R[x;z]  \mwedge{}  B[y]  \mwedge{}  B[z])  {}\mRightarrow{}  A[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  A[x]))


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}f,g,h,x.  let  y,RAorB  =  f  x 
                                                in  let  R,AorB  =  RAorB 
                                                      in  case  AorB
                                                              of  inl(A)  =>
                                                              (\mlambda{}k.let  y1,raORb  =  k  x 
                                                                      in  let  r,aORb  =  raORb 
                                                                            in  case  aORb  of  inl(a)  =>  g  x  y  y1  <R,  r,  A,  a>  |  inr(b)  =>  Ax\000C) 
                                                              f
                                                              |  inr(B)  =>
                                                              (\mlambda{}k.let  y1,raORb  =  k  x 
                                                                      in  let  r,aORb  =  raORb 
                                                                            in  case  aORb  of  inl(a)  =>  Ax  |  inr(b)  =>  h  x  y  y1  <R,  r,  B,  b>\000C) 
                                                              f\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index