Proof of Nuprl Lemma : reliable-env-property

Step * 1 1 1 1 1 4 2 of Lemma reliable-env-property

1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : 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(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S0;env;n2m;l2m))@i
9. n : ℕ@i
10. ∀n1:ℕn. ∀t:ℕ.
      ((run-command-node(pRun(S0;env;n2m;l2m);t;n1)
      ∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``))
      ⇒ (∃e:runEvents(pRun(S0;env;n2m;l2m))
           let t,n = <t, n1>
           in (run-info(pRun(S0;env;n2m;l2m);e)

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

              ∈ (ℤ × Id × pMsg(P.M[P])))
              ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Id)))@i
11. t : ℕ@i
12. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``)@i
14. t' : ℕ
15. t < t'
16. (fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n
17. ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');fst((env t' pRun(S0;env;n2m;l2m))))
    supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t'))
18. ∀i:ℕ
      ¬(t < i
      c∧ (((fst((env i pRun(S0;env;n2m;l2m)))) ≤ n)
         ∧ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m))))
           supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i))))
      supposing i < t'
19. k : ℕ@i
20. t + 0 < t'
⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + 0)))))
   ∧ (∀x:ℕ
        ((x ≤ n)
        ⇒ (run-command(pRun(S0;env;n2m;l2m);t + 0;x) = run-command(pRun(S0;env;n2m;l2m);t;x) ∈ pInTransit(P.M[P])))))
21. ∀k:{n:ℤ| 0 < n}
      ((t + (k - 1) < t'
       ⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1))))))
          ∧ (∀x:ℕ
               ((x ≤ n)
               ⇒ (run-command(pRun(S0;env;n2m;l2m);t + (k - 1);x)
                  = run-command(pRun(S0;env;n2m;l2m);t;x)
                  ∈ pInTransit(P.M[P]))))))
      ⇒ t + k < t'
      ⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k)))))
         ∧ (∀x:ℕ
              ((x ≤ n)
              ⇒ (run-command(pRun(S0;env;n2m;l2m);t + k;x)
                 = run-command(pRun(S0;env;n2m;l2m);t;x)
                 ∈ pInTransit(P.M[P]))))))
22. k1 : ℕ@i
23. t + k1 < t'
24. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k1)))))
25. x : ℕ@i
26. x ≤ n
⊢ run-command-node(pRun(S0;env;n2m;l2m);t + k1;x)
BY
{ (All (Unfold `run-command-node`) THEN Auto) }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : 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(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
8. reliable-env(env; pRun(S0;env;n2m;l2m))@i
9. n : ℕ@i
10. ∀n1:ℕn. ∀t:ℕ.
      ((n1 < lg-size(snd(snd((pRun(S0;env;n2m;l2m) t))))
      ∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``))
      ⇒ (∃e:runEvents(pRun(S0;env;n2m;l2m))
           let t,n = <t, n1>
           in (run-info(pRun(S0;env;n2m;l2m);e)

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

              ∈ (ℤ × Id × pMsg(P.M[P])))
              ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Id)))@i
11. t : ℕ@i
12. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) t))))@i
13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``)@i
14. t' : ℕ
15. t < t'
16. (fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n
17. ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');fst((env t' pRun(S0;env;n2m;l2m))))
    supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t'))
18. ∀i:ℕ
      ¬(t < i
      c∧ (((fst((env i pRun(S0;env;n2m;l2m)))) ≤ n)
         ∧ ↑lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m))))
           supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i))))
      supposing i < t'
19. k : ℕ@i
20. t + 0 < t'
⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + 0)))))
   ∧ (∀x:ℕ
        ((x ≤ n)
        ⇒ (run-command(pRun(S0;env;n2m;l2m);t + 0;x) = run-command(pRun(S0;env;n2m;l2m);t;x) ∈ pInTransit(P.M[P])))))
21. ∀k:{n:ℤ| 0 < n}
      ((t + (k - 1) < t'
       ⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1))))))
          ∧ (∀x:ℕ
               ((x ≤ n)
               ⇒ (run-command(pRun(S0;env;n2m;l2m);t + (k - 1);x)
                  = run-command(pRun(S0;env;n2m;l2m);t;x)
                  ∈ pInTransit(P.M[P]))))))
      ⇒ t + k < t'
      ⇒ (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k)))))
         ∧ (∀x:ℕ
              ((x ≤ n)
              ⇒ (run-command(pRun(S0;env;n2m;l2m);t + k;x)
                 = run-command(pRun(S0;env;n2m;l2m);t;x)
                 ∈ pInTransit(P.M[P]))))))
22. k1 : ℕ@i
23. t + k1 < t'
24. {n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k1)))))}
25. x : ℕ@i
26. {x ≤ n}
27. x ≤ n
⊢ lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k1))))) ∈ ℤ

Latex:

Latex:
1. M : Type {}\mrightarrow{} Type 2. Continuous+(P.M[P]) 3. S0 : 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(S0;env;n2m;l2m) \mmember{} pRunType(P.M[P]) 8. reliable-env(env; pRun(S0;env;n2m;l2m))@i 9. n : \mBbbN{}@i 10. \mforall{}n1:\mBbbN{}n. \mforall{}t:\mBbbN{}. ((run-command-node(pRun(S0;env;n2m;l2m);t;n1) \mwedge{} (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) \mmember{} ``msg choose new``)) {}\mRightarrow{} (\mexists{}e:runEvents(pRun(S0;env;n2m;l2m)) let t,n = <t, n1> in (run-info(pRun(S0;env;n2m;l2m);e) = intransit-to-info(n2m;l2m;pRun(S0;env;n2m;l2m);env;run-event-step(e);...)) \mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))))))@i 11. t : \mBbbN{}@i 12. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i 13. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) \mmember{} ``msg choose new``)@i 14. t' : \mBbbN{} 15. t < t' 16. (fst((env t' pRun(S0;env;n2m;l2m)))) \mleq{} n 17. \muparrow{}lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);t');fst((env t' pRun(S0;env;n2m;l2m)))) supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);t')) 18. \mforall{}i:\mBbbN{} \mneg{}(t < i c\mwedge{} (((fst((env i pRun(S0;env;n2m;l2m)))) \mleq{} n) \mwedge{} \muparrow{}lg-is-source(run-intransit(pRun(S0;env;n2m;l2m);i);fst((env i pRun(S0;env;n2m;l2m)))) supposing 0 < lg-size(run-intransit(pRun(S0;env;n2m;l2m);i)))) supposing i < t' 19. k : \mBbbN{}@i 20. t + 0 < t' {}\mRightarrow{} (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + 0))))) \mwedge{} (\mforall{}x:\mBbbN{} ((x \mleq{} n) {}\mRightarrow{} (run-command(pRun(S0;env;n2m;l2m);t + 0;x) = run-command(pRun(S0;env;n2m;l2m);t;x))))) 21. \mforall{}k:\{n:\mBbbZ{}| 0 < n\} ((t + (k - 1) < t' {}\mRightarrow{} (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + (k - 1)))))) \mwedge{} (\mforall{}x:\mBbbN{} ((x \mleq{} n) {}\mRightarrow{} (run-command(pRun(S0;env;n2m;l2m);t + (k - 1);x) = run-command(pRun(S0;env;n2m;l2m);t;x)))))) {}\mRightarrow{} t + k < t' {}\mRightarrow{} (n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k))))) \mwedge{} (\mforall{}x:\mBbbN{} ((x \mleq{} n) {}\mRightarrow{} (run-command(pRun(S0;env;n2m;l2m);t + k;x) = run-command(pRun(S0;env;n2m;l2m);t;x)))))) 22. k1 : \mBbbN{}@i 23. t + k1 < t' 24. n < lg-size(snd(snd((pRun(S0;env;n2m;l2m) (t + k1))))) 25. x : \mBbbN{}@i 26. x \mleq{} n \mvdash{} run-command-node(pRun(S0;env;n2m;l2m);t + k1;x) By Latex: (All (Unfold `run-command-node`) THEN Auto) Home Index