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