Step
*
of Lemma
cbv-concat-sq
∀[ll:Top List List]. (cbv-concat(ll) ~ concat(ll))
BY
{ Unfolds ``cbv-concat concat`` 0
THEN InductionOnList
THEN Reduce 0
THEN Try (Trivial)
THEN HypSubst' (-1) 0
THEN Thin (-1) }
1
1. u : Top List
2. v : Top List List
⊢ eval x = u in
eval y = reduce(λl,l'. (l @ l');[];v) in
x @ y ~ u @ reduce(λl,l'. (l @ l');[];v)
Latex:
Latex:
\mforall{}[ll:Top List List]. (cbv-concat(ll) \msim{} concat(ll))
By
Latex:
Unfolds ``cbv-concat concat`` 0
THEN InductionOnList
THEN Reduce 0
THEN Try (Trivial)
THEN HypSubst' (-1) 0
THEN Thin (-1)
Home
Index