Step
*
1
of Lemma
upto_decomp2
1. n : ℕ+
2. upto(n) ~ upto(1) @ map(λx.(x + 1);upto(n - 1))
⊢ upto(1) @ map(λx.(x + 1);upto(n - 1)) ~ [0 / map(λi.(i + 1);upto(n - 1))]
BY
{ Subst' upto(1) ~ [0] 0 }
1
.....equality.....
1. n : ℕ+
2. upto(n) ~ upto(1) @ map(λx.(x + 1);upto(n - 1))
⊢ upto(1) ~ [0]
2
1. n : ℕ+
2. upto(n) ~ upto(1) @ map(λx.(x + 1);upto(n - 1))
⊢ [0] @ map(λx.(x + 1);upto(n - 1)) ~ [0 / map(λi.(i + 1);upto(n - 1))]
Latex:
Latex:
1. n : \mBbbN{}\msupplus{}
2. upto(n) \msim{} upto(1) @ map(\mlambda{}x.(x + 1);upto(n - 1))
\mvdash{} upto(1) @ map(\mlambda{}x.(x + 1);upto(n - 1)) \msim{} [0 / map(\mlambda{}i.(i + 1);upto(n - 1))]
By
Latex:
Subst' upto(1) \msim{} [0] 0
Home
Index