2.2.3
Доказательство коммутативности сложения с 1:
суперкомпиляция предиката P
P
{
e
x
= <Eq (<Ad (e
x
) (I)>) (<Ad (I) (e
x
)>)>;
}
Ad
{
(e
x
)
(e
y
)
=
e
x
e
y
;
}
Eq
{
()
()
=
T;
(e
x
I)
(e
y
I)
=
<Eq (e
x
) (e
y
)>;
()
(e
y
I)
=
F;
(e
x
I)
()
=
F;
}
<P e
1
>
¯
<Eq (
<Ad (e
1
) (I)>
) (
<Ad (I) (e
1
)>
)>
¯
<Eq (e
1
I) (I e
1
)>
e
1
®
пусто
l
m
e
1
®
e
2
I
<Eq (I) (I)>
<Eq (e
2
I I
) (I e
2
I)>
¯
¯
<Eq () ())>
<Eq (e
1
I
) (I e
1
)>
¯
¯
T
e
1
:= e
2