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