[Imprint]
[Data Privacy Statement]
[E-Mail]
View
long theorem info
. View
the proof
. Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Proof step 1 from proof remove-contract (
previous step
)
# x0 = # rx0, # x1 = # rx1, x0 ≠ [], x1 ≠ [] ⊦ dls(head, prev, x0 + a ' + x1, rx0 + r ' + rx1, next, tail) = _∃(λ r0, r1. dls(head, prev, x0, rx0, r, r0) * r => mkcell(r0, r1, a) * dls(r1, r, x1, rx1, next, tail))
A spec-lemma