---

Step * 1 of Lemma psub_transitivity

.....assertion..... 
∀c,a,b:formula().  (a ⊆ b ⇒ b ⊆ c ⇒ a ⊆ c)
BY
{ ((BLemma `formula-induction` THENA Auto)
   THEN Unfold `psub` 0
   THEN Reduce 0
   THEN Fold `psub` 0
   THEN (Auto
         THEN SplitOrHyps
         THEN Try (((HypSubst' (-1) (-2) THENA Auto)
                    THEN Unfold `psub` -2
                    THEN Reduce (-2)
                    THEN Try (Fold `psub` (-2))
                    THEN Trivial))
         THEN Try (((InstHyp [⌜a⌝;⌜b⌝] 3⋅ THENM Sel 2 (D 0)) THEN Complete (Auto)))
         THEN Try (((InstHyp [⌜a⌝;⌜b⌝] 4⋅ THENM Sel 3 (D 0)) THEN Complete (Auto)))
         THEN Try (((InstHyp [⌜a⌝;⌜b⌝] 2⋅ THENM Sel 2 (D 0)) THEN Complete (Auto)))⋅)⋅) }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}c,a,b:formula().    (a  \msubseteq{}  b  {}\mRightarrow{}  b  \msubseteq{}  c  {}\mRightarrow{}  a  \msubseteq{}  c)


By

---

Latex:
((BLemma  `formula-induction`  THENA  Auto)
  THEN  Unfold  `psub`  0
  THEN  Reduce  0
  THEN  Fold  `psub`  0
  THEN  (Auto
              THEN  SplitOrHyps
              THEN  Try  (((HypSubst'  (-1)  (-2)  THENA  Auto)
                                    THEN  Unfold  `psub`  -2
                                    THEN  Reduce  (-2)
                                    THEN  Try  (Fold  `psub`  (-2))
                                    THEN  Trivial))
              THEN  Try  (((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  3\mcdot{}  THENM  Sel  2  (D  0))  THEN  Complete  (Auto)))
              THEN  Try  (((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  4\mcdot{}  THENM  Sel  3  (D  0))  THEN  Complete  (Auto)))
              THEN  Try  (((InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  2\mcdot{}  THENM  Sel  2  (D  0))  THEN  Complete  (Auto)))\mcdot{})\mcdot{})

---

Home Index