Step
*
of Lemma
list_2_decomp
∀[T:Type]. ∀[z:T List]. z = [z[0]; z[1]] ∈ (T List) supposing ||z|| = 2 ∈ ℕ
BY
{ (Auto' THEN RepeatFor 3 ((D -2 THEN All Reduce THEN Auto)) THEN Auto') }
Latex:
Latex:
\mforall{}[T:Type]. \mforall{}[z:T List]. z = [z[0]; z[1]] supposing ||z|| = 2
By
Latex:
(Auto' THEN RepeatFor 3 ((D -2 THEN All Reduce THEN Auto)) THEN Auto')
Home
Index