Quelle  list_props_aux.pvs

% Extras for list_props (prelude)
%
% Author: David Lester Manchester University 25/12/2007.

list_props_aux[T:TYPE]: THEORY

BEGIN

  l, l1, l2, l3: VAR list[T]
  x: VAR T

  length_is_0: LEMMA length(l) = 0 IFF l = null


  append_is_null: LEMMA null?(append(l1,l2)) IFF (null?(l1) AND null?(l2))

  append_eq1: LEMMA append(l1,l2) = append(l1,l3) IFF l2 = l3
  append_eq2: LEMMA append(l2,l1) = append(l3,l1) IFF l2 = l3

END list_props_aux