---

Step * of Lemma seq-normalize-normalize

∀[n,m:ℕ]. ∀[s:Top].  (seq-normalize(n;seq-normalize(m;s)) ~ seq-normalize(if (n) < (m)  then n  else m;s))
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualTopToBase
   THEN (RepUR ``seq-normalize`` 0
         THEN EqCD
         THEN RenameVar `k' (-1)
         THEN BoolCase ⌜n <z m⌝⋅
         THEN Reduce 0
         THEN Try (Complete (Auto)))
   THEN Try ((BLemma `less_sqequal` THEN Auto))) }

1
1. n : ℕ
2. m : ℕ
3. ¬n < m
4. s : Base
5. k : Base
⊢ if (k) < (n)  then if (k) < (m)  then s k  else ⊥  else ⊥ ~ if (k) < (m)  then s k  else ⊥

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbN{}].  \mforall{}[s:Top].
    (seq-normalize(n;seq-normalize(m;s))  \msim{}  seq-normalize(if  (n)  <  (m)    then  n    else  m;s))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualTopToBase
  THEN  (RepUR  ``seq-normalize``  0
              THEN  EqCD
              THEN  RenameVar  `k'  (-1)
              THEN  BoolCase  \mkleeneopen{}n  <z  m\mkleeneclose{}\mcdot{}
              THEN  Reduce  0
              THEN  Try  (Complete  (Auto)))
  THEN  Try  ((BLemma  `less\_sqequal`  THEN  Auto)))

---

Home Index