Nuprl - Proof: accumulate-induction1 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)) }

Q(j,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; } ;H(j,u);N(j,u)))

By: ((GenConclAtAddr [4;3]) THEN (GenConcl (H(j,u) = a))) THENA (Auto THEN Analyze) THEN Thin -1 THEN AssertBY z N(j,u) (BackThru Thm* L1,L2:T List. L1 = L2 L1 L2) THEN MoveToConcl -1 THEN MoveToConcl -1 THEN Thin -1 THEN ListInd -1 THEN Reduce 0

Generated subgoals:

1 25. z: B List
26. a: {s:A| M(s)M(H(j,u)) }
27. nil N(j,u)
Q(j,a,a) 1 step

2 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)
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)) 7 steps

About:

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

1	25. `z:` `B List` 26. `a:` `{s:A\| M(s)M(H(j,u)) }` 27. `nil N(j,u)` `Q(j,a,a)`	1 step

2	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)` `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))`	7 steps