Proof of Nuprl Lemma : reliable-env-property

Step * of Lemma reliable-env-property

∀[M:Type ─→ Type]

  ∀S0:InitialSystem(P.M[P]). ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀env:pEnvType(P.M[P]).

    let r = pRun(S0;env;n2m;l2m) in
        reliable-env(env; r)
        ⇒ (∀tn:run-msg-commands(r)
              ∃e:runEvents(r)
               let t,n = tn
               in (run-info(r;e)
                  = intransit-to-info(n2m;l2m;r;env;run-event-step(e);run-command(r;t;n))
                  ∈ (ℤ × Id × pMsg(P.M[P])))
                  ∧ (run-event-loc(e) = (fst(snd(run-command(r;t;n)))) ∈ Id))
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `reliable-env-property1` []
   THEN (RepeatFor 6 ((ParallelLast' THENA Auto))
         THEN All (RepUR ``let``)⋅
         THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
                     (DoSubsume THEN Auto))
         THEN ParallelOp -2)
   THEN (Auto
         THEN D -1
         THEN (RenameVar `n' (-1)
               THEN D -1
               THEN (Assert run-command-node(pRun(S0;env;n2m;l2m);t;n)

                           ∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``) BY

                           (Auto
                            THEN Try ((Unhide
                                       THEN Auto
                                       THEN GenConclAtAddr [2;1;1;1]
                                       THEN RepeatFor 2 (D -2)
                                       THEN Reduce 0
                                       THEN Auto))
                            THEN All (Unfold `run-command-node`)
                            THEN Auto))
               THEN Thin (-2)
               THEN (MoveToConcl (-1) THEN MoveToConcl (-2))
               THEN CompNatInd (-1)
               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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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'))
10. n : ℕ@i
11. ∀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
12. t : ℕ@i
13. run-command-node(pRun(S0;env;n2m;l2m);t;n)@i
14. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ ``msg choose new``)@i
⊢ ∃e:runEvents(pRun(S0;env;n2m;l2m))
   let t,n = <t, n>
   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(pRun(S0;env;n2m;l2m);t;n))

      ∈ (ℤ × Id × pMsg(P.M[P])))
      ∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Id)

2
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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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))))

              = 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
12. t : ℕ@i
13. run-command-node(pRun(S0;env;n2m;l2m);t;n)
⊢ com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) ∈ Atom

3
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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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'))
10. n : ℕ@i
11. n1 : ℕn@i
12. t : ℕ@i
13. run-command-node(pRun(S0;env;n2m;l2m);t;n1)
⊢ com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ Atom

4
.....set predicate.....
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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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'))
10. n : ℕ@i
11. n1 : ℕn@i
12. t : ℕ@i
13. run-command-node(pRun(S0;env;n2m;l2m);t;n1)
14. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``)
15. e : runEvents(pRun(S0;env;n2m;l2m))@i
16. t1 : ℕ
17. n2 : ℕn
18. <t, n1> = <t1, n2> ∈ (ℕ × ℕn)
⊢ 0 < run-event-step(e)

5
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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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'))
10. n : ℕ@i
11. ∀i:ℕ
      ((∀n1:ℕi. ∀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))))

      ⇒ (∀t:ℕ
            ((run-command-node(pRun(S0;env;n2m;l2m);t;i)
            ∧ (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;i)))) ∈ ``msg choose new``))
            ⇒ (∃e:runEvents(pRun(S0;env;n2m;l2m))
                 let t,n = <t, i>
                 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)))))

12. n1 : ℕ@i
13. t : ℕ@i
14. run-command-node(pRun(S0;env;n2m;l2m);t;n1)
⊢ com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ Atom

6
.....set predicate.....
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. ∀tn:run-msg-commands(pRun(S0;env;n2m;l2m))
     let t,n = tn
     in ∃t':ℕ
         ((t < t'
         c∧ (((fst((env t' pRun(S0;env;n2m;l2m)))) ≤ n)

            ∧ ↑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'))))
         ∧ (∀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))))

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

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

12. n1 : ℕ@i
13. t : ℕ@i
14. run-command-node(pRun(S0;env;n2m;l2m);t;n1)
15. (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n1)))) ∈ ``msg choose new``)
16. e : runEvents(pRun(S0;env;n2m;l2m))@i
17. t1 : ℕ
18. n2 : ℕ
19. <t, n1> = <t1, n2> ∈ (ℕ × ℕ)
⊢ 0 < run-event-step(e)

Latex:

Latex:
\mforall{}[M:Type {}\mrightarrow{} Type] \mforall{}S0:InitialSystem(P.M[P]). \mforall{}n2m:\mBbbN{} {}\mrightarrow{} pMsg(P.M[P]). \mforall{}l2m:Id {}\mrightarrow{} pMsg(P.M[P]). \mforall{}env:pEnvType(P.M[P]). let r = pRun(S0;env;n2m;l2m) in reliable-env(env; r) {}\mRightarrow{} (\mforall{}tn:run-msg-commands(r) \mexists{}e:runEvents(r) let t,n = tn in (run-info(r;e) = intransit-to-info(n2m;l2m;r;env;run-event-step(e);run-command(r;t;n))) \mwedge{} (run-event-loc(e) = (fst(snd(run-command(r;t;n)))))) supposing Continuous+(P.M[P]) By Latex: (InstLemma `reliable-env-property1` [] THEN (RepeatFor 6 ((ParallelLast' THENA Auto)) THEN All (RepUR ``let``)\mcdot{} THEN (Assert pRun(S0;env;n2m;l2m) \mmember{} pRunType(P.M[P]) BY (DoSubsume THEN Auto)) THEN ParallelOp -2) THEN (Auto THEN D -1 THEN (RenameVar `n' (-1) THEN D -1 THEN (Assert run-command-node(pRun(S0;env;n2m;l2m);t;n) \mwedge{} (com-kind(snd(snd(run-command(pRun(S0;env;n2m;l2m);t;n)))) \mmember{} ``msg choose new``) BY (Auto THEN Try ((Unhide THEN Auto THEN GenConclAtAddr [2;1;1;1] THEN RepeatFor 2 (D -2) THEN Reduce 0 THEN Auto)) THEN All (Unfold `run-command-node`) THEN Auto)) THEN Thin (-2) THEN (MoveToConcl (-1) THEN MoveToConcl (-2)) THEN CompNatInd (-1) THEN Auto)\mcdot{})\mcdot{}) Home Index