---

Step * of Lemma test-example4

∀[Dom:Type]. ∀[A,B,C,D,P,Q,G:Dom ⟶ ℙ]. ∀[R1,R2:Dom ⟶ Dom ⟶ ℙ].
  ((∀x:Dom. (A[x] ∨ B[x]))
  ⇒ (∀x:Dom. (C[x] ∨ D[x]))
  ⇒ (∀x:Dom. ((A[x] ∧ C[x]) ⇒ (∃y:Dom. (R1[x;y] ∧ P[y]))))
  ⇒ (∀x:Dom. ((A[x] ∧ D[x]) ⇒ (∃y:Dom. (R1[x;y] ∧ Q[y]))))
  ⇒ (∀x:Dom. ((B[x] ∧ C[x]) ⇒ (∃y:Dom. (R1[x;y] ∧ P[y]))))
  ⇒ (∀x:Dom. ((B[x] ∧ D[x]) ⇒ (∃y:Dom. (R1[x;y] ∧ Q[y]))))
  ⇒ (∀x:Dom. ((A[x] ∧ C[x]) ⇒ (∃y:Dom. (R2[x;y] ∧ Q[y]))))
  ⇒ (∀x:Dom. ((A[x] ∧ D[x]) ⇒ (∃y:Dom. (R2[x;y] ∧ P[y]))))
  ⇒ (∀x:Dom. ((B[x] ∧ C[x]) ⇒ (∃y:Dom. (R2[x;y] ∧ Q[y]))))
  ⇒ (∀x:Dom. ((B[x] ∧ D[x]) ⇒ (∃y:Dom. (R2[x;y] ∧ P[y]))))
  ⇒ (∀x,y,z:Dom.  (((R1[x;y] ∧ R2[x;z]) ∧ ((P[y] ∧ Q[z]) ∨ (Q[y] ∧ P[z]))) ⇒ G[x]))
  ⇒ (∀x:Dom. G[x]))
BY
{ (EvidenceTac ⌜λAB,CD,AC1,AD1,BC1,BD1,AC2,AD2,BC2,BD2,G,x. case CD x
                                                            of inl(C) =>
                                                            case AB x
                                                             of inl(A) =>
                                                             let y,R2Q = AC2 x <A, C> 
                                                             in let y1,R1P = AC1 x <A, C> 
                                                                in G x y1 y 
                                                                   let R1,P = R1P 
                                                                   in let R2,Q = R2Q 
                                                                      in <<R1, R2>, inl <P, Q>>
                                                             | inr(B) =>
                                                             let y,r2q = BC2 x <B, C> 
                                                             in let y1,r1p = BC1 x <B, C> 
                                                                in G x y1 y 
                                                                   let r1,p = r1p 
                                                                   in let R2,Q = r2q 
                                                                      in <<r1, R2>, inl <p, Q>>
                                                            | inr(D) =>
                                                            case AB x
                                                             of inl(A) =>
                                                             let y,r2p = AD2 x <A, D> 
                                                             in let y1,r1q = AD1 x <A, D> 
                                                                in G x y1 y 
                                                                   let R1,Q = r1q 
                                                                   in let R2,P = r2p 
                                                                      in <<R1, R2>, inr <Q, P> >
                                                             | inr(B) =>
                                                             let y,r2p = BD2 x <B, D> 
                                                             in let y1,r1q = BD1 x <B, D> 
                                                                in G x y1 y 
                                                                   let R1,Q = r1q 
                                                                   in let R2,P = r2p 
                                                                      in <<R1, R2>, inr <Q, P> >⌝⋅
   THENA Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[Dom:Type].  \mforall{}[A,B,C,D,P,Q,G:Dom  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R1,R2:Dom  {}\mrightarrow{}  Dom  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Dom.  (A[x]  \mvee{}  B[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  (C[x]  \mvee{}  D[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((A[x]  \mwedge{}  C[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R1[x;y]  \mwedge{}  P[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((A[x]  \mwedge{}  D[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R1[x;y]  \mwedge{}  Q[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((B[x]  \mwedge{}  C[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R1[x;y]  \mwedge{}  P[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((B[x]  \mwedge{}  D[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R1[x;y]  \mwedge{}  Q[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((A[x]  \mwedge{}  C[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R2[x;y]  \mwedge{}  Q[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((A[x]  \mwedge{}  D[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R2[x;y]  \mwedge{}  P[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((B[x]  \mwedge{}  C[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R2[x;y]  \mwedge{}  Q[y]))))
    {}\mRightarrow{}  (\mforall{}x:Dom.  ((B[x]  \mwedge{}  D[x])  {}\mRightarrow{}  (\mexists{}y:Dom.  (R2[x;y]  \mwedge{}  P[y]))))
    {}\mRightarrow{}  (\mforall{}x,y,z:Dom.    (((R1[x;y]  \mwedge{}  R2[x;z])  \mwedge{}  ((P[y]  \mwedge{}  Q[z])  \mvee{}  (Q[y]  \mwedge{}  P[z])))  {}\mRightarrow{}  G[x]))
    {}\mRightarrow{}  (\mforall{}x:Dom.  G[x]))


By

---

Latex:
(EvidenceTac  \mkleeneopen{}\mlambda{}AB,CD,AC1,AD1,BC1,BD1,AC2,AD2,BC2,BD2,G,x.  case  CD  x
                                                                                                                    of  inl(C)  =>
                                                                                                                    case  AB  x
                                                                                                                      of  inl(A)  =>
                                                                                                                      let  y,R2Q  =  AC2  x  <A,  C> 
                                                                                                                      in  let  y1,R1P  =  AC1  x  <A,  C> 
                                                                                                                            in  G  x  y1  y 
                                                                                                                                  let  R1,P  =  R1P 
                                                                                                                                  in  let  R2,Q  =  R2Q 
                                                                                                                                        in  <<R1,  R2>,  inl  <P,  Q>>
                                                                                                                      |  inr(B)  =>
                                                                                                                      let  y,r2q  =  BC2  x  <B,  C> 
                                                                                                                      in  let  y1,r1p  =  BC1  x  <B,  C> 
                                                                                                                            in  G  x  y1  y 
                                                                                                                                  let  r1,p  =  r1p 
                                                                                                                                  in  let  R2,Q  =  r2q 
                                                                                                                                        in  <<r1,  R2>,  inl  <p,  Q>>
                                                                                                                    |  inr(D)  =>
                                                                                                                    case  AB  x
                                                                                                                      of  inl(A)  =>
                                                                                                                      let  y,r2p  =  AD2  x  <A,  D> 
                                                                                                                      in  let  y1,r1q  =  AD1  x  <A,  D> 
                                                                                                                            in  G  x  y1  y 
                                                                                                                                  let  R1,Q  =  r1q 
                                                                                                                                  in  let  R2,P  =  r2p 
                                                                                                                                        in  <<R1,  R2>,  inr  <Q,  P>  >
                                                                                                                      |  inr(B)  =>
                                                                                                                      let  y,r2p  =  BD2  x  <B,  D> 
                                                                                                                      in  let  y1,r1q  =  BD1  x  <B,  D> 
                                                                                                                            in  G  x  y1  y 
                                                                                                                                  let  R1,Q  =  r1q 
                                                                                                                                  in  let  R2,P  =  r2p 
                                                                                                                                        in  <<R1,  R2>,  inr  <Q,  P>  >\mkleeneclose{}\mcdot{}
  THENA  Auto
  )

---

Home Index