set include BOOL off . fmod BubbleSort is protecting BOOL * (sort Bool to REC-Bool) . sorts Bool Nat NatList . op 0 : -> Nat . op cons : Nat NatList -> NatList . op fact : Nat -> Nat . op false : -> Bool . op lt : Nat Nat -> Bool . op nil : -> NatList . op plus : Nat Nat -> Nat . op rev : Nat -> NatList . op s : Nat -> Nat . op times : Nat Nat -> Nat . op true : -> Bool . eq fact(0) = s(0) . eq fact(s(N:Nat)) = times(s(N:Nat),fact(N:Nat)) . eq lt(0,s(N:Nat)) = (true).Bool . eq lt(N:Nat,N:Nat) = (false).Bool . eq lt(s(N:Nat),0) = (false).Bool . eq lt(s(N:Nat),s(M:Nat)) = lt(N:Nat,M:Nat) . eq plus(0,N:Nat) = N:Nat . eq plus(s(N:Nat),M:Nat) = s(plus(N:Nat,M:Nat)) . eq rev(0) = cons(0,nil) . eq rev(s(N:Nat)) = cons(s(N:Nat),rev(N:Nat)) . eq times(0,N:Nat) = 0 . eq times(s(N:Nat),M:Nat) = plus(M:Nat,times(N:Nat,M:Nat)) . ceq cons(N:Nat,cons(M:Nat,L:NatList)) = cons(M:Nat,cons(N:Nat,L:NatList)) if lt(M:Nat,N:Nat)=(true).Bool . endfm reduce rev(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(s(0))))))))))))))))))))) . reduce cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s( s(s(0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(0), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), cons(s(s(s(0))), cons(s(s(0)), cons(s(s(s(0))), cons(s(s(s(s(s(s( 0)))))), nil)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) . reduce rev(fact(s(s(s(s(s(0))))))) .