A,B:Type, M:(A), Q:(BAAProp), P:(BA), F,G,H:(BAA), N:(BA(B List)). (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. P(j,u) Q(j,u,F(j,u))) (j:B, u,z:A. P(j,u) Q(j,H(j,u),z) Q(j,u,G(j,z))) (j:B, u:A. Q(j,u,u)) (i,j:B, u,v,z:A. Q(i,u,v) Q(j,v,z) Q(j,u,z)) (j:B, u:A. 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; } ))

Auto
THEN
RepeatFor 2 (MoveToConcl -1)
THEN
Assert (m:, u:A. M(u) = m (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; } )))
THEN
Try (Complete (Auto THEN (Using [`m',M(u)] EasyHyp)))
THEN
CompleteInductionOnNat
THEN
RecUnfold `accumulate` 0
THEN
SplitOnConclITE
THEN
Try (Complete (Auto THEN EasyHyp))
THEN
Inst Thm* accumulate_wf [A;B;P;F;G;H;N;M]
THEN
Try Trivial
THEN
AssertBY (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)) }) (Auto THEN (Try (Analyze THEN (Complete Auto))) THEN (InstHyp [i';s'] -3) THEN (GenConclAtAddr [2]) THEN (Thin -1) THEN (Analyze -4) THEN (Analyze -1))
THEN
AllHyps (h.(BackThru h) THEN (Try (Complete Auto)) THEN (Try ((GenConclAtAddr [2]) THEN (Thin -1) THEN (Analyze -1) THEN (Complete Auto))))

1

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

9 steps

About: