1
2 (*** Addition with fixpoint of successor ***)
3
4 Ex3 = LCF +
5
6 consts
7 s :: "'a => 'a"
8 p :: "'a => 'a => 'a"
9
10 rules
11 p_strict "p(UU) = UU"
12 p_s "p(s(x),y) = s(p(x,y))"
13
14 end