Proof of Nuprl Lemma : reliable-env-property2

Step * 1 1 2 1 1 2 1 of Lemma reliable-env-property2

1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
     ∃e:runEvents(pRun(S;env;n2m;l2m))
      let t,n = tn
      in (run-info(pRun(S;env;n2m;l2m);e)

         = intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))

∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
10. t : ℕ@i
11. x : Id@i
12. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
13. \\%12 : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
14. P : Process(P.M[P])@i
15. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
16. 0 < t
17. v1 : ℤ × Id@i
18. ms : pMsg(P.M[P])@i

19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i

20. v2 : Process(P.M[P])@i
21. G : LabeledDAG(Id × pCom(P.M[P]))@i
22. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
23. n : ℕlg-size(G)@i
24. v3 : Id@i
25. v4 : pCom(P.M[P])@i
26. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
27. (com-kind(v4) ∈ ``msg choose new``)@i
28. ga : LabeledGraph(pInTransit(P.M[P]))
29. gb : LabeledGraph(pInTransit(P.M[P]))

30. (snd(snd((pRun(S;env;n2m;l2m) t)))) = lg-append(ga;lg-append(add-cause(<t, x>;G);gb)) ∈ LabeledGraph(pInTransit(P.M[\000CP]))

⊢ ∃m:ℕlg-size(lg-append(ga;lg-append(add-cause(<t, x>;G);gb))). (lg-label(lg-append(ga;lg-append(add-cause(<t, x>;G);gb)\000C);m) = lg-label(add-cause(<t, x>;G);n) ∈ pInTransit(P.M[P]))

BY
{ (Assert n < lg-size(add-cause(<t, x>;G)) BY
         (Unfold `add-cause` 0
          THEN (RepUR ``lg-size lg-map`` 0
                THEN RWO "length-map-sq" 0
                THEN Auto
                THEN Try ((Fold `lg-size` 0 THEN Auto))
                THEN RepeatFor 2 (DVar `G')
                THEN Trivial)⋅
          ))⋅ }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S;env;n2m;l2m))@i
9. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
     ∃e:runEvents(pRun(S;env;n2m;l2m))
      let t,n = tn
      in (run-info(pRun(S;env;n2m;l2m);e)

         = intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))

19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms> ∈ (ℤ × Id × pMsg(P.M[P]))@i

30. (snd(snd((pRun(S;env;n2m;l2m) t)))) = lg-append(ga;lg-append(add-cause(<t, x>;G);gb)) ∈ LabeledGraph(pInTransit(P.M[\000CP]))

31. n < lg-size(add-cause(<t, x>;G))

⊢ ∃m:ℕlg-size(lg-append(ga;lg-append(add-cause(<t, x>;G);gb))). (lg-label(lg-append(ga;lg-append(add-cause(<t, x>;G);gb)\000C);m) = lg-label(add-cause(<t, x>;G);n) ∈ pInTransit(P.M[P]))

Latex:

Latex:
1. [M] : Type {}\mrightarrow{} Type 2. Continuous+(P.M[P]) 3. S : InitialSystem(P.M[P])@i 4. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i 5. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i 6. env : pEnvType(P.M[P])@i 7. pRun(S;env;n2m;l2m) \mmember{} pRunType(P.M[P]) 8. reliable-env(env; pRun(S;env;n2m;l2m))@i 9. \mforall{}tn:run-msg-commands(pRun(S;env;n2m;l2m)) \mexists{}e:runEvents(pRun(S;env;n2m;l2m)) let t,n = tn in ... \mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n))))) 10. t : \mBbbN{}@i 11. x : Id@i 12. \mlambda{}c.fst(c) = x \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{} 13. \mbackslash{}\mbackslash{}\%12 : \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)@i 14. P : Process(P.M[P])@i 15. (P \mmember{} run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i 16. 0 < t 17. v1 : \mBbbZ{} \mtimes{} Id@i 18. ms : pMsg(P.M[P])@i 19. let info,S = pRun(S;env;n2m;l2m) t in let ev,z,m = outl(info) in <ev, m> = <v1, ms>@i 20. v2 : Process(P.M[P])@i 21. G : LabeledDAG(Id \mtimes{} pCom(P.M[P]))@i 22. Process-apply(P;ms) = <v2, G>@i 23. n : \mBbbN{}lg-size(G)@i 24. v3 : Id@i 25. v4 : pCom(P.M[P])@i 26. lg-label(G;n) = <v3, v4>@i 27. (com-kind(v4) \mmember{} ``msg choose new``)@i 28. ga : LabeledGraph(pInTransit(P.M[P])) 29. gb : LabeledGraph(pInTransit(P.M[P])) 30. (snd(snd((pRun(S;env;n2m;l2m) t)))) = lg-append(ga;lg-append(add-cause(<t, x>G);gb)) \mvdash{} \mexists{}m:\mBbbN{}lg-size(lg-append(ga;lg-append(add-cause(<t, x>G);gb))). (lg-label(lg-append(ga;lg-append(add\000C-cause(<t, x>G);gb));m) = lg-label(add-cause(<t, x>G);n)) By Latex: (Assert n < lg-size(add-cause(<t, x>G)) BY (Unfold `add-cause` 0 THEN (RepUR ``lg-size lg-map`` 0 THEN RWO "length-map-sq" 0 THEN Auto THEN Try ((Fold `lg-size` 0 THEN Auto)) THEN RepeatFor 2 (DVar `G') THEN Trivial)\mcdot{} ))\mcdot{} Home Index