| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/linear_algebra/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle more_list_props.pvs Sprache: PVS |
|||||||||
|
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.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28