AAProp
A
AA
AA
AA
A(B List)
i:B, s:A. P(i,s) 
M(F(i,s))
M(s)
i:B, s:A. M(G(i,s))M(s)
i:B, s:A. 
P(i,s) M(H(i,s)) < M(s)
j:B, u:A. P(j,u) Q(j,u,F(j,u))
j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))
j:B, u:A. Q(j,u,u)
i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)
m1:.
m1 < m
(u:A.
M(u) = m1
(j:B.
Q(j
,u
,process u j where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
} )))
P(j,u)
j:B, u:A.
process u j where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
}
{s:A| M(s)M(u) }
{s:A| M(s)M(H(j,u)) }
a:{s:A| M(s)M(H(j,u)) }.
v 
N(j,u)
Q(j
,a
,list_accum(s',i'.process s' i' where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
} ;a;v))
M(H(j,u)) }
N(j,u)
Q(j,a,list_accum(s',i'.process s' i' where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ;process a u1 where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ;v))
h.(InstHyp [M(a);a;u1] h) THENA (Auto THEN (Analyze -2) THEN (AssertBY (M(H(j,u)) < M(u)) EasyHyp) THEN (Complete Auto)))
| 1 | 31. Q(u1
,a
,process a u1 where
process s i ==
if P(i,s) then F(i,s)
else G(i,s) where
xs := N(i,s);
s:= H(i,s);
while not null xs {
s := process s (hd xs);
xs := tl xs;
} ) Q(j,a,list_accum(s',i'.process s' i' where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ;process a u1 where process s i == if P(i,s) then F(i,s) else G(i,s) where xs := N(i,s); s:= H(i,s); while not null xs { s := process s (hd xs); xs := tl xs; } ;v)) | 6 steps |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |