Step
*
of Lemma
quicksort-int-length
∀[L:ℤ List]. (||L|| = ||quicksort-int(L)|| ∈ ℤ)
BY
{ (Auto
THEN (InstLemma `quicksort-int_wf` [⌜L⌝]⋅ THENA Auto)
THEN DVarSets
THEN Auto
THEN FLemma `permutation-length` [-1]
THEN Auto) }
Latex:
Latex:
\mforall{}[L:\mBbbZ{} List]. (||L|| = ||quicksort-int(L)||)
By
Latex:
(Auto
THEN (InstLemma `quicksort-int\_wf` [\mkleeneopen{}L\mkleeneclose{}]\mcdot{} THENA Auto)
THEN DVarSets
THEN Auto
THEN FLemma `permutation-length` [-1]
THEN Auto)
Home
Index