---

Step * of Lemma bar-val-stable

∀[T:Type]. ∀[n:ℕ]. ∀[x:bar-base(T)].
  ∀[m:ℤ]. bar-val(m;x) = bar-val(n;x) ∈ (T?) supposing n ≤ m supposing ↑isl(bar-val(n;x))
BY
{ ((InductionOnNat THEN (D 0 THENA Auto))
   THEN ((GenConcl ⌜x = Z ∈ (T + bar-base(T))⌝⋅ THENA (Auto THEN DoSubsume THEN Auto))
         THEN Thin (-1)
         THEN D -1
         THEN RecUnfold `bar-val` 0
         THEN Reduce 0
         THEN Try (AutoSplit)
         THEN (Auto THEN AutoSplit THEN BackThruSomeHyp THEN Auto)⋅)⋅
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[x:bar-base(T)].
    \mforall{}[m:\mBbbZ{}].  bar-val(m;x)  =  bar-val(n;x)  supposing  n  \mleq{}  m  supposing  \muparrow{}isl(bar-val(n;x))


By

---

Latex:
((InductionOnNat  THEN  (D  0  THENA  Auto))
  THEN  ((GenConcl  \mkleeneopen{}x  =  Z\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
              THEN  Thin  (-1)
              THEN  D  -1
              THEN  RecUnfold  `bar-val`  0
              THEN  Reduce  0
              THEN  Try  (AutoSplit)
              THEN  (Auto  THEN  AutoSplit  THEN  BackThruSomeHyp  THEN  Auto)\mcdot{})\mcdot{}
  )

---

Home Index