---

Step * 1 of Lemma prank-psub


1. a : formula()
⊢ ∀b:formula(). (a ⊆ b ⇒ ((a = b ∈ formula()) ∨ prank(a) < prank(b)))
BY
{ ((BLemma `formula-induction` THENA Auto)
   THEN Unfolds ``psub prank`` 0
   THEN Reduce 0
   THEN Folds ``psub prank`` 0
   THEN Auto
   THEN Try ((ParallelLast THEN SplitOrHyps THEN ThinTrivial))
   THEN Try ((D -1 THEN xxx((RWO "imax_unfold" 0 THENA Auto) THEN OldAutoSplit THEN HypSubst' (-2) 0 THEN Auto)xxx)⋅)) }

1
1. a : formula()
2. sub : formula()
3. a ⊆ sub
4. (a = sub ∈ formula()) ∨ prank(a) < prank(sub)
⊢ prank(a) < prank(sub) + 1

---

Latex:

---

Latex:

1.  a  :  formula()
\mvdash{}  \mforall{}b:formula().  (a  \msubseteq{}  b  {}\mRightarrow{}  ((a  =  b)  \mvee{}  prank(a)  <  prank(b)))


By

---

Latex:
((BLemma  `formula-induction`  THENA  Auto)
  THEN  Unfolds  ``psub  prank``  0
  THEN  Reduce  0
  THEN  Folds  ``psub  prank``  0
  THEN  Auto
  THEN  Try  ((ParallelLast  THEN  SplitOrHyps  THEN  ThinTrivial))
  THEN  Try  ((D  -1
                        THEN  xxx((RWO  "imax\_unfold"  0  THENA  Auto)
                                          THEN  OldAutoSplit
                                          THEN  HypSubst'  (-2)  0
                                          THEN  Auto)xxx
                        )\mcdot{}))

---

Home Index