Proof of Nuprl Lemma : adjacent-run-states

Step * 1 2 2 2 1 1 of Lemma adjacent-run-states

1. ∀[M:Type ─→ Type]

     ∀x:Id. ∀v3:component(P.M[P]) List. ∀v11:Id. ∀k:ℕ. ∀ms:pMsg(P.M[P]). ∀G:LabeledDAG(pInTransit(P.M[P])).

       (Continuous+(P.M[P])
       ⇒ (¬↑x = v11)
       ⇒ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = deliver-msg(k;ms;v11;v3;G)

                                                    in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))

2. [M] : Type ─→ Type
3. Continuous+(P.M[P])
4. n2m : ℕ ─→ pMsg(P.M[P])@i
5. l2m : Id ─→ pMsg(P.M[P])@i
6. S : System(P.M[P])@i
7. env : pEnvType(P.M[P])@i
8. x : Id@i
9. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
10. n : ℤ@i
11. \\%3 : 0 < n@i
12. ∀t:ℕ⁺
      ((∀a:runEvents(pRun(S;env;n2m;l2m))
          ((run-event-loc(a) = x ∈ Id) ⇒ (¬((t ≤ run-event-step(a)) ∧ run-event-step(a) < t + (n - 1)))))
      ⇒

 run-event-state-when(pRun(S;env;n2m;l2m);<t, x>) ⊆ run-event-state-when(pRun(S;env;n2m;l2m);<t + (n - 1), x>))@\000Ci

13. t : ℕ⁺@i
14. (t + n) - 1 ≠ 0
15. ∀a:runEvents(pRun(S;env;n2m;l2m))
      ((run-event-loc(a) = x ∈ Id) ⇒ (¬((t ≤ run-event-step(a)) ∧ run-event-step(a) < t + n)))@i
⊢ (¬↑let info,S = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in
     do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1)));n@0;m;nm)
     in isl(info) ∧_b let ev,z,m = outl(info) in x = z)
⇒ let info,Cs,G = pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1) in

   mapfilter(λc.(snd(c));λc.fst(c) = x;Cs) ⊆ let info,Cs,G = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in

   do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1)));n@0;m;nm) in
   mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
BY
{ ((GenConclAtAddr [2;2;1] THENA Auto')
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN (GenConclAtAddr [2;3;1;1] THENA Auto')⋅
   THEN RepeatFor 2 (D -2)
   THEN Reduce 0
   THEN RepUR ``do-chosen-command`` 0
   THEN AutoSplit
   THEN Try ((RepUR ``bfalse`` 0 THEN Auto THEN BLemma `l_contains_weakening` THEN Auto)⋅)
   THEN (GenConclAtAddrType ⌈pInTransit(P.M[P])⌉ [2;3;1;1]⋅
         THENA (Auto THEN RepUR ``lg-is-source`` (-1) THEN SplitOnHypITE -1  THEN Auto)
         )
   THEN RepeatFor 2 (D (-2))
   THEN RepUR ``let`` 0
   THEN Repeat (AutoSplit)
   THEN RepUR ``bfalse`` 0

   THEN Try ((RepUR ``create-component`` 0 THEN Auto THEN BLemma `mapfilter-contains` THEN Auto THEN D 0 THEN Auto)⋅)

THEN (RepUR ``spreadn`` 0 THEN (Auto THEN BHyp 1 THEN Auto THEN Auto')⋅)⋅) }

Latex:

Latex:
1. \mforall{}[M:Type {}\mrightarrow{} Type] \mforall{}x:Id. \mforall{}v3:component(P.M[P]) List. \mforall{}v11:Id. \mforall{}k:\mBbbN{}. \mforall{}ms:pMsg(P.M[P]). \mforall{}G:LabeledDAG(pInTransit(P.M[P])). (Continuous+(P.M[P]) {}\mRightarrow{} (\mneg{}\muparrow{}x = v11) {}\mRightarrow{} mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;v3) \msubseteq{} let Cs,G = deliver-msg(k;ms;v11;v3;G) in mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs)) 2. [M] : Type {}\mrightarrow{} Type 3. Continuous+(P.M[P]) 4. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i 5. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i 6. S : System(P.M[P])@i 7. env : pEnvType(P.M[P])@i 8. x : Id@i 9. \mlambda{}c.fst(c) = x \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{} 10. n : \mBbbZ{}@i 11. \mbackslash{}\mbackslash{}\%3 : 0 < n@i 12. \mforall{}t:\mBbbN{}\msupplus{} ((\mforall{}a:runEvents(pRun(S;env;n2m;l2m)) ((run-event-loc(a) = x) {}\mRightarrow{} (\mneg{}((t \mleq{} run-event-step(a)) \mwedge{} run-event-step(a) < t + (n - 1))))) {}\mRightarrow{} run-event-state-when(pRun(S;env;n2m;l2m);<t, x>) \msubseteq{} run-event-state-when(pRun(S;env;n2m;l2m)\000C;<t + (n - 1), x>))@i 13. t : \mBbbN{}\msupplus{}@i 14. (t + n) - 1 \mneq{} 0 15. \mforall{}a:runEvents(pRun(S;env;n2m;l2m)) ((run-event-loc(a) = x) {}\mRightarrow{} (\mneg{}((t \mleq{} run-event-step(a)) \mwedge{} run-event-step(a) < t + n)))@i \mvdash{} (\mneg{}\muparrow{}let info,S = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1)));n@0;m;nm) in isl(info) \mwedge{}\msubb{} let ev,z,m = outl(info) in x = z) {}\mRightarrow{} let info,Cs,G = pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1) in mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs) \msubseteq{} let info,Cs,G = let n@0,m,nm = env ((t + n) - 1) pRun(S;env;n2m;l2m) in do-chosen-command(n2m;l2m;(t + n) - 1;snd((pRun(S;env;n2m;l2m) ((t + (n - 1)) - 1))); n@0;m;nm) in mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs) By Latex: ((GenConclAtAddr [2;2;1] THENA Auto') THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN (GenConclAtAddr [2;3;1;1] THENA Auto')\mcdot{} THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN RepUR ``do-chosen-command`` 0 THEN AutoSplit THEN Try ((RepUR ``bfalse`` 0 THEN Auto THEN BLemma `l\_contains\_weakening` THEN Auto)\mcdot{}) THEN (GenConclAtAddrType \mkleeneopen{}pInTransit(P.M[P])\mkleeneclose{} [2;3;1;1]\mcdot{} THENA (Auto THEN RepUR ``lg-is-source`` (-1) THEN SplitOnHypITE -1 THEN Auto) ) THEN RepeatFor 2 (D (-2)) THEN RepUR ``let`` 0 THEN Repeat (AutoSplit) THEN RepUR ``bfalse`` 0 THEN Try ((RepUR ``create-component`` 0 THEN Auto THEN BLemma `mapfilter-contains` THEN Auto THEN D 0 THEN Auto)\mcdot{}) THEN (RepUR ``spreadn`` 0 THEN (Auto THEN BHyp 1 THEN Auto THEN Auto')\mcdot{})\mcdot{}) Home Index