Nuprl - Proof: accumulate wf

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

A,B:Type, P:(BA), F,G,H:(BAA), N:(BA(B List)), M:(A). (i:B, s:A. P(i,s) M(F(i,s))M(s)) (i:B, s:A. M(G(i,s))M(s)) (i:B, s:A. P(i,s) M(H(i,s)) < M(s)) (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) })

By: Auto THEN RepeatFor 2 (MoveToConcl -1) THEN Assert (m:, u:A. M(u) = m (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) })) THEN Try (Complete (Auto THEN (Using [`m',M(u)] EasyHyp))) THEN CompleteInductionOnNat THEN RecUnfold `accumulate` 0 THEN SplitOnConclITE THEN Try (Complete (Auto THEN Analyze THEN EasyHyp))

Generated subgoal:

1 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)
G(j,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(u) } 9 steps

About:

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