Step * of Lemma Wmul-assoc

[A:Type]. ∀[B:A ⟶ Type]. ∀[zero,succ:A ⟶ 𝔹]. ∀[w3,w2,w1:W(A;a.B[a])].
  (w1 (w2 w3)) ((w1 w2) w3) ∈ W(A;a.B[a]) 
  supposing ∀a:A. (((↑(succ a))  (Unit ⊆B[a])) ∧ ((↑(zero a))  B[a])))
BY
(Auto⋅
   THEN RepeatFor (MoveToConcl (-2))
   THEN UseWInductionLemma
   THEN Auto
   THEN RW (AddrC [2;4] RecUnfoldTopAbC) 0
   THEN RW (AddrC [3] RecUnfoldTopAbC) 0
   THEN Unfold `Wsup` 0
   THEN Reduce 0
   THEN Fold `Wsup` 0
   THEN AutoSplit) }

1
1. Type
2. A ⟶ Type
3. zero A ⟶ 𝔹
4. succ A ⟶ 𝔹
5. ∀a:A. (((↑(succ a))  (Unit ⊆B[a])) ∧ ((↑(zero a))  B[a])))
6. A
7. ¬↑(succ a)
8. B[a] ⟶ W(A;a.B[a])
9. ∀b:B[a]. ∀w2,w1:W(A;a.B[a]).  ((w1 (w2 b)) ((w1 w2) b) ∈ W(A;a.B[a]))
10. w2 W(A;a.B[a])
11. w1 W(A;a.B[a])
⊢ (w1 Wsup(a;λx.(w2 x))) Wsup(a;λx.((w1 w2) x)) ∈ 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)  *  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  (-2))
  THEN  UseWInductionLemma
  THEN  Auto
  THEN  RW  (AddrC  [2;4]  RecUnfoldTopAbC)  0
  THEN  RW  (AddrC  [3]  RecUnfoldTopAbC)  0
  THEN  Unfold  `Wsup`  0
  THEN  Reduce  0
  THEN  Fold  `Wsup`  0
  THEN  AutoSplit)




Home Index