None
Conclusion:
x.(
%1.%1 (
x) x Ax)
(
x1.(
%1.%1 (x1 + 1) x1 Ax)
(
zz.(
%1.(
%1.(
%.(
%2.%2 %1)
I(%) where I(
) =
when zzj =
< 0, % = I(
+1).
%2.Ax
when
= 0.
%,x1,%.(
%1.Ax) x1
when zzj =
> 0, % = I(
-1).
%2,x1,%@0.
(
%3,x,%.
(
%4.(
%5.%5 %4)
case x
of inl(x2) =>
%,y.
case y
of inl(x3) => (
%1.case %1
of inl(%) => inl Ax
| inr(%2) => inr (
%.any (
%2
Ax))
)
((
%1.%1 x2 x3)
ext{decidable__equal_Var})
| inr(y2) => case y2
of inl(x3) => inr (
%.(
%1.Ax)
Ax)
| inr(y3) => case y3
of inl(x3) => let
<x4,x5> = x3
in
inr
(
%.(
%1.Ax)
Ax)
| inr(y4) => case
y4
of i
nl(x3) => let <x4,x5> = x3
in
inr (
%.(
%1.Ax)
Ax)
| i
nr(y5) => let <y6,y7> = y5
in
inr (
%.(
%1.Ax)
Ax)
| inr(y) => case y
of inl(x1) =>
%,y@0.
case y@0
of inl(x2) => inr (
%1.(
%2.Ax)
Ax)
| inr(y) => case y
of inl(x2) => case %
x
1
A
x
x
2
of inl
(%) => inl Ax
| inr
(%2) => inr (
%.any (%2
Ax))
| inr(y1) => case y
1
of inl
(x2) => let <x3,x4> = x2
in
inr (
%1.(
%2.Ax)
Ax)
| inr
(y) => case y
of inl(x2) => let <x3,x4> = x2
in
inr (
%1.(
%2.Ax)
Ax)
| inr(y1) => let <y2,y3> = y1
in
inr (
%1.(
%2.Ax)
Ax)
| inr(y1) => case y1
of inl(x1) => let <x2,x3> = x1
in
%.(
%1,y@0.
case y@0
of inl(x4) => i
nr (
%4.(
%5.Ax)
Ax)
| inr(y) => ca
se y
of
inl(x4) => inr (
%4.(
%5.Ax)
Ax)
|
inr(y1) => case y1
of inl(x4) => let <x5,x6> = x4
in
case %1
x2
Ax
x5
of inl(%@0) => case %
x3
Ax
x6
of inl(%6) => inl Ax
| inr(%7) => inr (
%8.any (%7
Ax))
| inr(%6) => inr (
%.any (%6
Ax))
| inr(y) => case y
of inl(x4) => let <x5,x6> = x4
in
inr (
%4.(
%5.Ax)
Ax)
| inr(y1) => let <y2,y3> = y1
in
inr (
%4.(
%5.Ax)
Ax) )
%
| inr(y) => case y
of inl(x1) => let <x2
,x3> = x1
in
%.(
%1
,y@0.
ca
se y@0
of
inl(x4) => inr (
%4.(
%5.Ax)
Ax)
|
inr(y) => case y
of inl(x4) => inr (
%4.(
%5.Ax)
Ax)
| inr(y1) => case y1
of inl(x4) => let <x5,x6> = x4
in
inr (
%4.(
%5.Ax)
Ax)
| inr(y) => case y
of inl(x4) => let <x5,x6> = x4
in
case %1
x2
Ax
x5
of inl(%@0) => case %
x3
Ax
x6
of inl(%6) => inl Ax
| inr(%7) => inr (
%8.any (%7
Ax))
| inr(%6) => inr (
%.any (%6
Ax))
| inr(y1) => let <y2,y3> = y1
in
inr (
%4.(
%5.Ax)
Ax) )
%
| inr(y1) => let <y2
,y3> = y1
in
%.(
%1
,y@0.
ca
se y@0
of
inl(x1) => inr (
%4.(
%5.Ax)
Ax)
|
inr(y) => case y
of inl(x1) => inr (
%4.(
%5.Ax)
Ax)
| inr(y3@0) => case y3@0
of inl(x1) => let <x2,x3> = x1
in
inr (
%4.(
%5.Ax)
Ax)
| inr(y) => case y
of inl(x1) => let <x2,x3> = x1
in
inr (
%4.(
%5.Ax)
Ax)
| inr(y3@0) => let <y4,y5> = y3@0
in
case %1
y2
Ax
y4
of inl(%@0) => case %
y3
Ax
y5
of inl(%6) => inl Ax
| inr(%7) => inr (
%8.any (%
7
Ax))
| inr(%6) => inr (
%.any (%6
Ax)) )
%)
(
x2,%4.%3 (
x2) Ax x2 Ax))
(
x2,%3.% (
.Ax) x2 Ax)
end where )
zz)
(%1 zz))
ext{nat_properties}))