Nuprl - Proof: accumulate wf 1 2

(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. 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) }

By: Thin -1 THEN Analyze -1 THEN Analyze THEN AssertBY (M(G(j,a))M(a)) EasyHyp THEN AssertBY (M(H(j,u)) < M(u)) EasyHyp

Generated subgoals:

None

About:

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