(10steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

At: accumulate wf 1
1. A: Type
2. B: Type
3. P: BA
4. F: BAA
5. G: BAA
6. H: BAA
7. N: BA(B List)
8. M: A
9. i:B, s:A. P(i,s) M(F(i,s))M(s)
10. i:B, s:A. M(G(i,s))M(s)
11. i:B, s:A. P(i,s) M(H(i,s)) < M(s)
12. m:
13. m1:. m1 < m (u:A. M(u) = m1 (j:B. 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) }))
14. u: A
15. M(u) = m
16. j: B
17. P(j,u)
G(j,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; } ;H(j,u);N(j,u))) {s:A| M(s)M(u) }
By:
GenConcl (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; } ;H(j,u);N(j,u)) = a)
THEN
Try (Complete Auto)
Generated subgoals:

1 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; } ;H(j,u);N(j,u)) {s:A| M(s)M(H(j,u)) }7 steps
 
218. a: {s:A| M(s)M(H(j,u)) }
19. 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; } ;H(j,u);N(j,u)) = a {s:A| M(s)M(H(j,u)) }
G(j,a) {s:A| M(s)M(u) }		1 step

About:
listboolassertless_thansetfunctionuniverseequalmemberimpliesall

(10steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc