---

Step * 1 1 of Lemma Wmul-Wadd


1. A : Type
2. B : A ⟶ Type
3. zero : A ⟶ 𝔹
4. succ : A ⟶ 𝔹
5. ∀a:A. (((↑(succ a)) ⇒ (Unit ⊆r B[a])) ∧ ((↑(zero a)) ⇒ (¬B[a])))
6. a : A
7. f : B[a] ⟶ W(A;a.B[a])
8. ∀b:B[a]. ∀w2,w1:W(A;a.B[a]).  ((w1 * (w2 + f b)) = ((w1 * w2) + (w1 * f b)) ∈ W(A;a.B[a]))
9. w2 : W(A;a.B[a])
10. w1 : W(A;a.B[a])
11. ↑(zero a)
12. ↑(zero a)
⊢ (w1 * w2) = ((w1 * w2) + (w1 * Wsup(a;f))) ∈ W(A;a.B[a])
BY
{ ((RW (AddrC [3] RecUnfoldTopAbC) 0 THEN RW (AddrC [3;1] RecUnfoldTopAbC) 0)
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN Fold `Wsup` 0
   THEN AutoSplit
   THEN Try ((Unfold `Wsup` 0 THEN Reduce 0 THEN Fold `Wsup` 0 THEN AutoSplit)⋅))⋅ }

1
1. A : Type
2. B : A ⟶ Type
3. zero : A ⟶ 𝔹
4. succ : A ⟶ 𝔹
5. ∀a:A. (((↑(succ a)) ⇒ (Unit ⊆r B[a])) ∧ ((↑(zero a)) ⇒ (¬B[a])))
6. a : A
7. f : B[a] ⟶ W(A;a.B[a])
8. ∀b:B[a]. ∀w2,w1:W(A;a.B[a]).  ((w1 * (w2 + f b)) = ((w1 * w2) + (w1 * f b)) ∈ W(A;a.B[a]))
9. w2 : W(A;a.B[a])
10. w1 : W(A;a.B[a])
11. ↑(zero a)
12. ↑(zero a)
13. ↑(succ a)
⊢ (w1 * w2)
= let a,f = ((w1 * f ⋅) + w1) 
  in if zero a then (w1 * w2) else Wsup(a;λx.((w1 * w2) + f x)) fi 
∈ W(A;a.B[a])

---

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]))  \mwedge{}  ((\muparrow{}(zero  a))  {}\mRightarrow{}  (\mneg{}B[a])))
6.  a  :  A
7.  f  :  B[a]  {}\mrightarrow{}  W(A;a.B[a])
8.  \mforall{}b:B[a].  \mforall{}w2,w1:W(A;a.B[a]).    ((w1  *  (w2  +  f  b))  =  ((w1  *  w2)  +  (w1  *  f  b)))
9.  w2  :  W(A;a.B[a])
10.  w1  :  W(A;a.B[a])
11.  \muparrow{}(zero  a)
12.  \muparrow{}(zero  a)
\mvdash{}  (w1  *  w2)  =  ((w1  *  w2)  +  (w1  *  Wsup(a;f)))


By

---

Latex:
((RW  (AddrC  [3]  RecUnfoldTopAbC)  0  THEN  RW  (AddrC  [3;1]  RecUnfoldTopAbC)  0)
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit
  THEN  Try  ((Unfold  `Wsup`  0  THEN  Reduce  0  THEN  Fold  `Wsup`  0  THEN  AutoSplit)\mcdot{}))\mcdot{}

---

Home Index