Proof of Nuprl Lemma : adjacent-run-states

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

1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. S : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. x : Id@i
8. pRun(S;env;n2m;l2m) ∈ pRunType(P.M[P])
9. n : ℤ@i
10. \\%3 : 0 < n@i
11. ∀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

12. t : ℕ⁺@i
13. ∀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
14. ∀[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))

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

BY
{ (PromoteHyp (-1) 1
   THEN RepUR ``run-event-state-when`` 0
   THEN RW (AddrC [3] (RecUnfoldC `pRun`)) 0
   THEN Reduce 0
   THEN (Assert ¬↑is-run-event(pRun(S;env;n2m;l2m);(t + n) - 1;x) BY
               ((D 0 THEN Auto')
                THEN OnMaybeHyp 12 (\h. ((InstHyp [⌈<(t + n) - 1, x>⌉] h⋅

                                         THENM (D -1 THEN RepUR ``run-event-step`` 0 THEN Complete (Auto'))

)
THENA (Auto

                                                THEN Try ((MemTypeCD THEN Auto THEN Auto'))

                                                THEN RepUR ``run-event-loc`` 0

                                                THEN Complete (Auto))
                                         ))
                )))⋅ }

1
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. pRun(S;env;n2m;l2m) ∈ pRunType(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. ∀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
15. ¬↑is-run-event(pRun(S;env;n2m;l2m);(t + n) - 1;x)
⊢ 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 = if ((t + n) - 1 =_z 0)
  then <inr ⋅ , S>
  else 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)
  fi  in
  mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)

Latex:

Latex:
1. [M] : Type {}\mrightarrow{} Type 2. Continuous+(P.M[P]) 3. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i 4. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i 5. S : System(P.M[P])@i 6. env : pEnvType(P.M[P])@i 7. x : Id@i 8. pRun(S;env;n2m;l2m) \mmember{} pRunType(P.M[P]) 9. n : \mBbbZ{}@i 10. \mbackslash{}\mbackslash{}\%3 : 0 < n@i 11. \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 12. t : \mBbbN{}\msupplus{}@i 13. \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 14. \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)) \mvdash{} run-event-state-when(pRun(S;env;n2m;l2m);<t + (n - 1), x>) \msubseteq{} run-event-state-when(pRun(S;env;n2m;l\000C2m);<t + n, x>) By Latex: (PromoteHyp (-1) 1 THEN RepUR ``run-event-state-when`` 0 THEN RW (AddrC [3] (RecUnfoldC `pRun`)) 0 THEN Reduce 0 THEN (Assert \mneg{}\muparrow{}is-run-event(pRun(S;env;n2m;l2m);(t + n) - 1;x) BY ((D 0 THEN Auto') THEN OnMaybeHyp 12 (\mbackslash{}h. ((InstHyp [\mkleeneopen{}<(t + n) - 1, x>\mkleeneclose{}] h\mcdot{} THENM (D -1 THEN RepUR ``run-event-step`` 0 THEN Complete (Auto')) ) THENA (Auto THEN Try ((MemTypeCD THEN Auto THEN Auto')) THEN RepUR ``run-event-loc`` 0 THEN Complete (Auto)) )) )))\mcdot{} Home Index