---

Step * of Lemma Wmul-Wadd

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹].
  ∀[w3,w2,w1:W(A;a.B[a])].  ((w1 * (w2 + w3)) = ((w1 * w2) + (w1 * w3)) ∈ W(A;a.B[a])) 
  supposing ∀a:A. (((↑(succ a)) ⇒ (Unit ⊆r B[a])) ∧ ((↑(zero a)) ⇒ (¬B[a])))
BY
{ (Auto⋅ THEN RepeatFor 3 (MoveToConcl (-1)) THEN UseWInductionLemma THEN Auto THEN (Decide ↑(zero a) THENA Auto)) }

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)
⊢ (w1 * (w2 + Wsup(a;f))) = ((w1 * w2) + (w1 * Wsup(a;f))) ∈ W(A;a.B[a])

2
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)
⊢ (w1 * (w2 + Wsup(a;f))) = ((w1 * w2) + (w1 * Wsup(a;f))) ∈ W(A;a.B[a])

---

Latex:

---

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


By

---

Latex:
(Auto\mcdot{}
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  (Decide  \muparrow{}(zero  a)  THENA  Auto))

---

Home Index