fmod LIST is
protecting INT .
---
op equal : Int Int -> Bool .
ceq equal(N, M) 
   = true
   if N <= M = true /\ M <= N = true .
ceq equal(N, M) 
   = false
   if N < M = true .
ceq equal(N, M) 
   = false
   if M < N = true .
---
sorts List .
op nil : -> List [ctor] .
op _:_ : Int List -> List [ctor] .
op member : Int List -> Bool .
op append : List List -> List .
op rev : List -> List .
vars N M N1 N2 : Int .
vars L L1 L2 : List .
---
--- append
---
eq append(nil, L) = L .
eq append(N : L1, L2)
   = N : append(L1, L2) .
---
--- member
---
eq member(N, nil)
   = false .
ceq member(N1, N2 : L)
    = true
    if equal(N1, N2) = true . 
ceq member(N1, N2 : L)
    = member(N1, L)
    if equal(N1, N2) = false . 
---
--- rev
---
eq rev(nil) = nil .
eq rev(N : L)
   = append(rev(L), N : nil) .
endfm

--- Start ITP
select ITP-TOOL .
loop init-itp .

--- Theorem to prove
(goal rev-append : 
   LIST |- A{L1:List ; L2:List}
           ((rev(append(L1:List, L2:List))) 
             = (append(rev(L2:List), rev(L1:List)))) .)