---

Step * of Lemma Wleq-Wmul

∀[A:Type]. ∀[B:A ⟶ Type].
  ∀zero,succ:A ⟶ 𝔹.
    ((∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a])))
    ⇒ (∀a:A. (¬↑(zero a) ⇐⇒ B[a]))
    ⇒ (∀w3,w2,w1:W(A;a.B[a]).  ((w1 ≤  w2) ⇒ ((w1 * w3) ≤  (w2 * w3)))))
BY
{ (RepeatFor 6 ((D 0 THENA Auto))
   THEN UseWInductionLemma
   THEN Auto
   THEN RecUnfold `Wmul` 0
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN Fold `Wsup` 0
   THEN AutoSplit
   THEN Try ((RepeatFor 2 ((ReduceWcmp 0 THEN Auto)) THEN With ⌜x⌝ (D 0)⋅ THEN Auto))) }

1
1. [A] : Type
2. [B] : A ⟶ Type
3. zero : A ⟶ 𝔹
4. succ : A ⟶ 𝔹
5. ∀a:A. ((↑(succ a)) ⇒ (Unit ⊆r B[a]))
6. ∀a:A. (¬↑(zero a) ⇐⇒ B[a])
7. a : A
8. f : B[a] ⟶ W(A;a.B[a])
9. ∀b:B[a]. ∀w2,w1:W(A;a.B[a]).  ((w1 ≤  w2) ⇒ ((w1 * f b) ≤  (w2 * f b)))
10. w2 : W(A;a.B[a])
11. w1 : W(A;a.B[a])
12. w1 ≤  w2
13. ↑(succ a)
⊢ ((w1 * f ⋅) + w1) ≤  ((w2 * f ⋅) + w2)

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].
    \mforall{}zero,succ:A  {}\mrightarrow{}  \mBbbB{}.
        ((\mforall{}a:A.  ((\muparrow{}(succ  a))  {}\mRightarrow{}  (Unit  \msubseteq{}r  B[a])))
        {}\mRightarrow{}  (\mforall{}a:A.  (\mneg{}\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  B[a]))
        {}\mRightarrow{}  (\mforall{}w3,w2,w1:W(A;a.B[a]).    ((w1  \mleq{}    w2)  {}\mRightarrow{}  ((w1  *  w3)  \mleq{}    (w2  *  w3)))))


By

---

Latex:
(RepeatFor  6  ((D  0  THENA  Auto))
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  RecUnfold  `Wmul`  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit
  THEN  Try  ((RepeatFor  2  ((ReduceWcmp  0  THEN  Auto))  THEN  With  \mkleeneopen{}x\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))

---

Home Index