set include BOOL off . fmod Fibonacci is protecting BOOL * (sort Bool to REC-Bool) . sorts Nat . op 0 : -> Nat . op fibb : Nat -> Nat . op plus : Nat Nat -> Nat . op s : Nat -> Nat . eq fibb(0) = s(0) . eq fibb(s(0)) = s(0) . eq fibb(s(s(N:Nat))) = plus(fibb(s(N:Nat)),fibb(N:Nat)) . eq plus(0,N:Nat) = N:Nat . eq plus(s(N:Nat),M:Nat) = s(plus(N:Nat,M:Nat)) . endfm reduce fibb(fibb(s(s(s(s(s(0))))))) . ----% s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0)))))))))))))))))))))))))))))))))) reduce fibb(fibb(fibb(s(s(s(s(s(0)))))))) .