type 'a list
logic nil : 'a list
logic cons : 'a, 'a list -> 'a list
logic first : 'a list -> 'a
logic rest : 'a list -> 'a list
logic append : 'a list, 'a list -> 'a list
logic reverse : 'a list -> 'a list
axiom F1: forall h: 'a. forall t: 'a list. first(cons(h,t))=h
axiom R1: forall h: 'a. forall t: 'a list. rest(cons(h,t))=t
axiom A: forall l: 'a list. 
         (not((l=nil))  -> l=cons(first(l),rest(l)))
axiom AppNil: forall l1: 'a list. append(l1,nil)=l1
axiom NilApp: forall l1: 'a list. append(nil,l1)=l1
axiom AppCons: forall h: 'a. forall t, l2: 'a list. append(cons(h,t),l2)=cons(h,append(t,l2))
axiom RevNil: reverse(nil)=nil
axiom RevCons: forall h: 'a. forall l1: 'a list. reverse(cons(h,l1))=append(reverse(l1),cons(h,nil))
axiom RevRev: forall l: 'a list. reverse(reverse(l))=l
axiom RevApp: forall l1, l2: 'a list. reverse(append(l1,l2))=append(reverse(l2),reverse(l1))
axiom Assoc: forall l1, l2, l3: 'a list. append(append(l1,l2),l3)=append(l1,append(l2,l3))

logic inp, out, temp: int list

goal intra_loop:
(not((temp=nil)) and 
inp=append(reverse(out),temp)  ->
     inp=append(reverse(cons(first(temp),out)),rest(temp)))


goal exit:
(temp=nil and 
inp=append(reverse(out),temp)  ->
     out=reverse(inp))


goal start:
(true  ->
     inp=append(reverse(nil),inp))