|
more_list_props[T: TYPE]: THEORY
BEGIN
x: VAR T
l1, l2, l3: VAR list[T]
P, Q: VAR PRED[T]
i: VAR nat
append1(l1, x): list[T] = append(l1, cons(x, null))
length_parm: LEMMA
FORALL (pl: list[(P)]):
length[(P)](pl) = length[T](pl)
nth_parm: LEMMA
FORALL (pl: list[(P)], (n:below[length(pl)])):
nth[(P)](pl, n) = nth[T](pl, n)
every_parm: LEMMA
FORALL (pl: list[(P)]):
every[(P)](Q)(pl) = every[T](Q)(pl)
append_parm: LEMMA
FORALL (l1, l2: list[(P)]):
append[(P)](l1, l2) = append[T](l1, l2)
append_append_cons: LEMMA
append(l1, cons(x, l2)) = append(append(l1, cons(x, null)), l2)
append_equal_null: LEMMA append(l1, l2) = l2 => l1 = null
nth_append_below: LEMMA
i < length(l1) => nth(append(l1, l2), i) = nth(l1, i)
nth_append_above: LEMMA
i >= length(l1) and i < length(append(l1, l2)) => nth(append(l1, l2), i) = nth(l2, i - length(l1))
tail?(l1, l2): recursive bool =
if null?(l1)
then null?(l2)
else l1 = l2 or tail?(cdr(l1), l2)
endif
measure l1 by <<
tail_append: lemma tail?(append(l1, l2), l2)
ldiff(l1, (l2 | tail?(l1, l2))): recursive list[T] =
if l1 = l2
then null
else cons(car(l1), ldiff(cdr(l1), l2))
endif
measure l1 by <<
ldiff_append: lemma forall (l1, l2): ldiff(append(l1, l2), l2) = l1
END more_list_props
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
