Nuprl - Proof: accumulate wf 1 1 1

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

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)
18. z: B List
19. a: {s:A| M(s)M(H(j,u)) }

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;z) {s:A| M(s)M(a) }

By: MoveToConcl -1 THEN ListInd -1 THEN Reduce 0

Generated subgoals:

1 19. u1: B
20. v: B List
21. a:{s:A| M(s)M(H(j,u)) }. 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) {s:A| M(s)M(a) }
22. a: {s:A| M(s)M(H(j,u)) }
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; } {s:A| M(s)M(a) } 1 step

2 19. u1: B
20. v: B List
21. a:{s:A| M(s)M(H(j,u)) }. 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) {s:A| M(s)M(a) }
22. a: {s:A| M(s)M(H(j,u)) }
23. s': {s:A| M(s)M(a) }
24. i': B
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; } {s:A| M(s)M(a) } 4 steps

About:

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

1	19. `u1:` `B` 20. `v:` `B List` 21. `a:{s:A\| M(s)M(H(j,u)) }. 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) {s:A\| M(s)M(a) }` 22. `a:` `{s:A\| M(s)M(H(j,u)) }` `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; } {s:A\| M(s)M(a) }`	1 step

2	19. `u1:` `B` 20. `v:` `B List` 21. `a:{s:A\| M(s)M(H(j,u)) }. 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) {s:A\| M(s)M(a) }` 22. `a:` `{s:A\| M(s)M(H(j,u)) }` 23. `s':` `{s:A\| M(s)M(a) }` 24. `i':` `B` `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; } {s:A\| M(s)M(a) }`	4 steps