type sequence

logic head : sequence -> int
logic tail : sequence -> sequence
logic cons : int, sequence -> sequence
logic seqnil : sequence

predicate is_seqnil(s:sequence) = s = seqnil

axiom seq_head :
forall s:sequence. forall i:int.
head(cons(i,s)) = i

axiom seq_tail :
forall s:sequence. forall i:int.
tail(cons(i,s)) = s

logic seq_length : sequence -> int 

axiom seq_length_cons :
forall s:sequence. forall i:int.
seq_length(cons(i,s)) = 1 + seq_length(s)

axiom seq_length_nil :
seq_length(seqnil) = 0


parameter why_head :
s: sequence ->
{ not is_seqnil(s) } int { result=head(s) }

parameter why_tail :
s: sequence ->
{ s <> seqnil } sequence { result=tail(s) }

parameter why_is_seqnil :
s: sequence ->
{ } bool { if result then is_seqnil(s) else (not is_seqnil(s)) }
