---

Step * 1 of Lemma Wleq-Wmul


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)
BY
{ ((FHyp 5 [-1] THENA Auto)
   THEN Using [`w2',⌜((w2 * f ⋅) + w1)⌝] (BLemma `Wcmp_transitivity`)⋅
   THEN Auto
   THEN (BLemma `Wleq-Wadd` ORELSE BLemma `Wleq-Wadd2`⋅)
   THEN Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  A  {}\mrightarrow{}  Type
3.  zero  :  A  {}\mrightarrow{}  \mBbbB{}
4.  succ  :  A  {}\mrightarrow{}  \mBbbB{}
5.  \mforall{}a:A.  ((\muparrow{}(succ  a))  {}\mRightarrow{}  (Unit  \msubseteq{}r  B[a]))
6.  \mforall{}a:A.  (\mneg{}\muparrow{}(zero  a)  \mLeftarrow{}{}\mRightarrow{}  B[a])
7.  a  :  A
8.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
9.  \mforall{}b:B[a].  \mforall{}w2,w1:W(A;a.B[a]).    ((w1  \mleq{}    w2)  {}\mRightarrow{}  ((w1  *  f  b)  \mleq{}    (w2  *  f  b)))
10.  w2  :  W(A;a.B[a])
11.  w1  :  W(A;a.B[a])
12.  w1  \mleq{}    w2
13.  \muparrow{}(succ  a)
\mvdash{}  ((w1  *  f  \mcdot{})  +  w1)  \mleq{}    ((w2  *  f  \mcdot{})  +  w2)


By

---

Latex:
((FHyp  5  [-1]  THENA  Auto)
  THEN  Using  [`w2',\mkleeneopen{}((w2  *  f  \mcdot{})  +  w1)\mkleeneclose{}]  (BLemma  `Wcmp\_transitivity`)\mcdot{}
  THEN  Auto
  THEN  (BLemma  `Wleq-Wadd`  ORELSE  BLemma  `Wleq-Wadd2`\mcdot{})
  THEN  Auto)

---

Home Index