---

Step * 1 of Lemma rec-value_subype_base

.....assertion..... 
∀n:ℕ. ∀v:rec-value().  ((rec-value-height(v) ≤ n) ⇒ (v ∈ Base))
BY
{ TACTIC:(CompleteInductionOnNat
          THEN Auto
          THEN ExtD 3
          THEN RepeatFor 2 (D 3)
          THEN All Reduce
          THEN (Declaration
          ORELSE (Unfold `rec-value-height` -1
                  THEN RecUnfold `co-value-height` (-1)
                  THEN Reduce (-1)
                  THEN Fold `rec-value-height` (-1)
                  THEN InstHyp [⌜n - 1⌝] 2⋅
                  THEN Auto)
          )) }

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}n:\mBbbN{}.  \mforall{}v:rec-value().    ((rec-value-height(v)  \mleq{}  n)  {}\mRightarrow{}  (v  \mmember{}  Base))


By

---

Latex:
TACTIC:(CompleteInductionOnNat
                THEN  Auto
                THEN  ExtD  3
                THEN  RepeatFor  2  (D  3)
                THEN  All  Reduce
                THEN  (Declaration
                ORELSE  (Unfold  `rec-value-height`  -1
                                THEN  RecUnfold  `co-value-height`  (-1)
                                THEN  Reduce  (-1)
                                THEN  Fold  `rec-value-height`  (-1)
                                THEN  InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  2\mcdot{}
                                THEN  Auto)
                ))

---

Home Index