---

Step * of Lemma sq_or_sq_or

∀[a,b,c:ℙ].  ({uiff(a ↓∨ b ↓∨ c;a ↓∨ (b ∨ c))} ∧ {uiff((b ↓∨ c) ↓∨ a;(b ∨ c) ↓∨ a)})
BY
{ (RepUR ``sq_or guard`` 0
   THEN Auto
   THEN SquashExRepD
   THEN SplitOrHyps
   THEN SquashExRepD
   THEN SplitOrHyps
   THEN D 0
   THEN ((((Sel 1 (D 0)⋅ THENA Auto)
           THEN Complete (Repeat (First [Trivial; D 0; Sel 1 (D 0) THEN Complete Auto
                                        ;Sel 2 (D 0) THEN Complete Auto]⋅))
           )⋅
         ORELSE ((Sel 2 (D 0)⋅ THENA Auto)
                 THEN Complete (Repeat (First [Trivial; D 0; Sel 1 (D 0) THEN Complete Auto
                                              ;Sel 2 (D 0) THEN Complete Auto]⋅))
                 )⋅
         )
   ORELSE (Sel 3 (D 0) THEN Auto)
   )) }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbP{}].    (\{uiff(a  \mdownarrow{}\mvee{}  b  \mdownarrow{}\mvee{}  c;a  \mdownarrow{}\mvee{}  (b  \mvee{}  c))\}  \mwedge{}  \{uiff((b  \mdownarrow{}\mvee{}  c)  \mdownarrow{}\mvee{}  a;(b  \mvee{}  c)  \mdownarrow{}\mvee{}  a)\})


By

---

Latex:
(RepUR  ``sq\_or  guard``  0
  THEN  Auto
  THEN  SquashExRepD
  THEN  SplitOrHyps
  THEN  SquashExRepD
  THEN  SplitOrHyps
  THEN  D  0
  THEN  ((((Sel  1  (D  0)\mcdot{}  THENA  Auto)
                  THEN  Complete  (Repeat  (First  [Trivial;  D  0;  Sel  1  (D  0)  THEN  Complete  Auto
                                                                            ;Sel  2  (D  0)  THEN  Complete  Auto]\mcdot{}))
                  )\mcdot{}
              ORELSE  ((Sel  2  (D  0)\mcdot{}  THENA  Auto)
                              THEN  Complete  (Repeat  (First  [Trivial;  D  0;  Sel  1  (D  0)  THEN  Complete  Auto
                                                                                        ;Sel  2  (D  0)  THEN  Complete  Auto]\mcdot{}))
                              )\mcdot{}
              )
  ORELSE  (Sel  3  (D  0)  THEN  Auto)
  ))

---

Home Index