Nuprl - Proof: accumulate-induction1 1 1

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

1. A: Type
2. B: Type
3. M: A
4. Q: BAAProp
5. P: BA
6. F: BAA
7. G: BAA
8. H: BAA
9. N: BA(B List)
10. i:B, s:A. P(i,s) M(F(i,s))M(s)
11. i:B, s:A. M(G(i,s))M(s)
12. i:B, s:A. P(i,s) M(H(i,s)) < M(s)
13. j:B, u:A. P(j,u) Q(j,u,F(j,u))
14. j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))
15. j:B, u:A. Q(j,u,u)
16. i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)
17. m:
18. 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; } )))
19. u: A
20. M(u) = m
21. j: B
22. P(j,u)
23. 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) }
24. 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)) }
25. z: B List
26. a: {s:A| M(s)M(H(j,u)) }
27. nil N(j,u)

Q(j,a,a)

By: EasyHyp

Generated subgoals:

None

About:

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