Step
*
1
1
of Lemma
unzip-as-accum
1. u1 : Top
2. u2 : Top
3. v : (Top × Top) List
4. b1 : Top List
5. b2 : Top List
⊢ <b1 @ [u1 / map(λp.(fst(p));v)], b2 @ [u2 / map(λp.(snd(p));v)]> ~ <(b1 @ [u1]) @ map(λp.(fst(p));v)
, (b2 @ [u2]) @ map(λp.(snd(p));v)
>
BY
{ xxx((RWO "append_assoc_sq" 0 THENM Reduce 0) THEN Auto)xxx }
Latex:
Latex:
1. u1 : Top
2. u2 : Top
3. v : (Top \mtimes{} Top) List
4. b1 : Top List
5. b2 : Top List
\mvdash{} <b1 @ [u1 / map(\mlambda{}p.(fst(p));v)], b2 @ [u2 / map(\mlambda{}p.(snd(p));v)]> \msim{} <(b1 @ [u1]) @ map(\mlambda{}p.(fst(p));\000Cv)
, (b2 @ [u2])
@ map(\mlambda{}p.(snd(p));v)
>
By
Latex:
xxx((RWO "append\_assoc\_sq" 0 THENM Reduce 0) THEN Auto)xxx
Home
Index