Nuprl - Proof: accumulate-induction1 1 2 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. u1: B
27. v: B List
28. 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))
29. a: {s:A| M(s)M(H(j,u)) }
30. [u1 / v] N(j,u)
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))

By: AssertBY (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) }) EasyHyp THEN Using [`i',u1;`v',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; } ] (BackThru 16) THEN Try (Complete ((GenConclAtAddr [2]) THEN (Analyze -2)))

Generated subgoals:

1 32. 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) }
33. s': A
34. 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; } A 1 step

2 32. 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) }
Q(j,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; } ,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)) 4 steps

About:

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

1	32. `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) }` 33. `s':` `A` 34. `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; } A`	1 step

2	32. `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) }` Q(j,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; } ,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))	4 steps