Proof of Nuprl Lemma : pRun

Step * 1 2 2 1 1 1 1 of Lemma pRun_functionality

1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
      (system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
      ∧ ((pRun(S1;env;nat2msg;loc2msg) t)
        = (pRun(S2;env;nat2msg;loc2msg) t)
        ∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. (P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P])))
∧ (||P5|| = ||P7|| ∈ ℤ)
∧ (∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q)@i
17. n : ℕ@i
18. m : ℕ@i
19. x : Id@i
20. ↑lg-is-source(P6;n)
21. ↑lg-is-source(P8;n)
⊢ system-equiv(P.M[P];snd(let ev,x@0,c = lg-label(P6;n) in
                      let G' = lg-remove(P6;n) in
                          if com-kind(c) =a "msg"
                            then let ms = comm-msg(c) in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

                          if com-kind(c) =a "create"
                            then let P = comm-create(c) in
                                     <inr ⋅ , create-component(t;P;x@0;P5;G')>
                          if com-kind(c) =a "choose"
                            then let ms = nat2msg m in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

if com-kind(c) =a "new"
then let ms = loc2msg x in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

                          else <inr ⋅ , P5, G'>
                          fi );snd(let ev,x@0,c = lg-label(P8;n) in
                      let G' = lg-remove(P8;n) in
                          if com-kind(c) =a "msg"
                            then let ms = comm-msg(c) in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

                          if com-kind(c) =a "create"
                            then let P = comm-create(c) in
                                     <inr ⋅ , create-component(t;P;x@0;P7;G')>
                          if com-kind(c) =a "choose"
                            then let ms = nat2msg m in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

if com-kind(c) =a "new"
then let ms = loc2msg x in

                                     <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

                          else <inr ⋅ , P7, G'>
                          fi ))
∧ (let ev,x@0,c = lg-label(P6;n) in
  let G' = lg-remove(P6;n) in

      if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

      if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x@0;P5;G')>

      if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

      if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>

      else <inr ⋅ , P5, G'>
      fi
  = let ev,x@0,c = lg-label(P8;n) in
    let G' = lg-remove(P8;n) in

        if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

        if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x@0;P7;G')>

        if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

        if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>

        else <inr ⋅ , P7, G'>
        fi
  ∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ ((GenConcl ⌈lg-remove(P6;n) = G1 ∈ LabeledDAG(pInTransit(P.M[P]))⌉⋅ THENA Auto)
   THEN (GenConcl ⌈lg-remove(P8;n) = G2 ∈ LabeledDAG(pInTransit(P.M[P]))⌉⋅ THENA Auto)
   THEN (Assert G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P])) BY
               Auto)
   THEN RepUR ``let`` 0
   THEN (Assert n < lg-size(P6) BY

               OnMaybeHyp 21 (\h. (RepUR ``lg-is-source`` h THEN SplitOnHypITE h  THEN Complete (Auto))))

THEN (Assert n < lg-size(P8) BY

               OnMaybeHyp 22 (\h. (RepUR ``lg-is-source`` h THEN SplitOnHypITE h  THEN Complete (Auto))))

   THEN (GenConcl ⌈lg-label(P6;n) = L1 ∈ pInTransit(P.M[P])⌉⋅ THENA Auto)⋅
   THEN ((GenConcl ⌈lg-label(P8;n) = L2 ∈ pInTransit(P.M[P])⌉⋅ THENA Auto)
         THEN (Assert L1 = L2 ∈ pInTransit(P.M[P]) BY
                     Auto)
         THEN ThinVar `n')⋅) }

1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
      (system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
      ∧ ((pRun(S1;env;nat2msg;loc2msg) t)
        = (pRun(S2;env;nat2msg;loc2msg) t)
        ∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. (P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P])))
∧ (||P5|| = ||P7|| ∈ ℤ)
∧ (∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q)@i
17. m : ℕ@i
18. x : Id@i
19. G1 : LabeledDAG(pInTransit(P.M[P]))@i
20. G2 : LabeledDAG(pInTransit(P.M[P]))@i
21. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
22. L1 : pInTransit(P.M[P])@i
23. L2 : pInTransit(P.M[P])@i
24. L1 = L2 ∈ pInTransit(P.M[P])
⊢ system-equiv(P.M[P];snd(let ev,x@0,c = L1 in

                      if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>

                      if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P5;G1)>

                      if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>

                      if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>

else <inr ⋅ , P5, G1>
fi );snd(let ev,x@0,c = L2 in

                      if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>

                      if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P7;G2)>

                      if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>

                      if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>

                      else <inr ⋅ , P7, G2>
                      fi ))
∧ (let ev,x@0,c = L1 in
  if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>
  if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P5;G1)>
  if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>
  if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>
  else <inr ⋅ , P5, G1>
  fi
  = let ev,x@0,c = L2 in
    if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>
    if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P7;G2)>
    if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>
    if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>
    else <inr ⋅ , P7, G2>
    fi
  ∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))

Latex:

Latex:
1. M : Type {}\mrightarrow{} Type 2. Continuous+(P.M[P]) 3. nat2msg : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P]) 4. loc2msg : Id {}\mrightarrow{} pMsg(P.M[P]) 5. env : pEnvType(P.M[P]) 6. S1 : System(P.M[P]) 7. S2 : System(P.M[P]) 8. system-equiv(P.M[P];S1;S2) 9. t : \{1...\} 10. \mforall{}t:\mBbbN{}t (system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t))) \mwedge{} ((pRun(S1;env;nat2msg;loc2msg) t) = (pRun(S2;env;nat2msg;loc2msg) t)))@i 11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) 12. P5 : component(P.M[P]) List@i 13. P6 : LabeledDAG(pInTransit(P.M[P]))@i 14. P7 : component(P.M[P]) List@i 15. P8 : LabeledDAG(pInTransit(P.M[P]))@i 16. (P6 = P8) \mwedge{} (||P5|| = ||P7||) \mwedge{} (\mforall{}k:\mBbbN{}||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z) \mwedge{} P\mequiv{}Q)@i 17. n : \mBbbN{}@i 18. m : \mBbbN{}@i 19. x : Id@i 20. \muparrow{}lg-is-source(P6;n) 21. \muparrow{}lg-is-source(P8;n) \mvdash{} system-equiv(P.M[P];snd(let ev,x@0,c = lg-label(P6;n) in let G' = lg-remove(P6;n) in if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> if com-kind(c) =a "create" then let P = comm-create(c) in <inr \mcdot{} , create-component(t;P;x@0;P5;G')> if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> else <inr \mcdot{} , P5, G'> fi );snd(let ev,x@0,c = lg-label(P8;n) in let G' = lg-remove(P8;n) in if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> if com-kind(c) =a "create" then let P = comm-create(c) in <inr \mcdot{} , create-component(t;P;x@0;P7;G')> if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> else <inr \mcdot{} , P7, G'> fi )) \mwedge{} (let ev,x@0,c = lg-label(P6;n) in let G' = lg-remove(P6;n) in if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> if com-kind(c) =a "create" then let P = comm-create(c) in <inr \mcdot{} , create-component(t;P;x@0;P5;G')> if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')> else <inr \mcdot{} , P5, G'> fi = let ev,x@0,c = lg-label(P8;n) in let G' = lg-remove(P8;n) in if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> if com-kind(c) =a "create" then let P = comm-create(c) in <inr \mcdot{} , create-component(t;P;x@0;P7;G')> if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')> else <inr \mcdot{} , P7, G'> fi ) By Latex: ((GenConcl \mkleeneopen{}lg-remove(P6;n) = G1\mkleeneclose{}\mcdot{} THENA Auto) THEN (GenConcl \mkleeneopen{}lg-remove(P8;n) = G2\mkleeneclose{}\mcdot{} THENA Auto) THEN (Assert G1 = G2 BY Auto) THEN RepUR ``let`` 0 THEN (Assert n < lg-size(P6) BY OnMaybeHyp 21 (\mbackslash{}h. (RepUR ``lg-is-source`` h THEN SplitOnHypITE h THEN Complete (Auto)))) THEN (Assert n < lg-size(P8) BY OnMaybeHyp 22 (\mbackslash{}h. (RepUR ``lg-is-source`` h THEN SplitOnHypITE h THEN Complete (Auto)))) THEN (GenConcl \mkleeneopen{}lg-label(P6;n) = L1\mkleeneclose{}\mcdot{} THENA Auto)\mcdot{} THEN ((GenConcl \mkleeneopen{}lg-label(P8;n) = L2\mkleeneclose{}\mcdot{} THENA Auto) THEN (Assert L1 = L2 BY Auto) THEN ThinVar `n') \mcdot{}) Home Index