Proof of Nuprl Lemma : pRun-invariant1

Step * 1 1 1 of Lemma pRun-invariant1

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. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in

     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))

                   then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

    if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

    if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

    if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>
    else <inr ⋅ , v5, lg-remove(v6;v1)>
    fi
    in isl(info) ∧_b let ev,z,m = outl(info) in x = z)
⇒ (fst(fst(let info,S = if com-kind(v10) =a "msg"

                           then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>

            else <inr ⋅ , v5, lg-remove(v6;v1)>
            fi
            in let ev,z,m = outl(info) in
               <ev, m>)) < t
   ∨ (∃m:ℕlg-size(S2)
       ((fst(let info,S = if com-kind(v10) =a "msg"

                            then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>

             else <inr ⋅ , v5, lg-remove(v6;v1)>
             fi
             in let ev,z,m = outl(info) in
                <ev, m>))
       = (fst(lg-label(S2;m)))
       ∈ (ℤ × Id))))
BY
{ Assert ⌈(↑x = v9) ⇒ (fst(v7) < t ∨ (∃m:ℕlg-size(S2). (v7 = (fst(lg-label(S2;m))) ∈ (ℤ × Id))))⌉⋅ }

1
.....assertion.....
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. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
     let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in

     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))

9. <S1, S2> ∈ System(P.M[P])
10. t : {1...}
11. x : Id@i
12. v1 : ℕ@i
13. v3 : ℕ@i
14. v4 : Id@i
15. (env t pRun(<S1, S2>;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
16. v5 : component(P.M[P]) List@i
17. v6 : LabeledDAG(pInTransit(P.M[P]))@i
18. (snd((pRun(<S1, S2>;env;n2m;l2m) (t - 1)))) = <v5, v6> ∈ System(P.M[P])@i
19. ↑null(lg-in-edges(v6;v1))
20. v1 < lg-size(v6)
21. v7 : ℤ × Id@i
22. v9 : Id@i
23. v10 : pCom(P.M[P])@i
24. lg-label(v6;v1) = <v7, v9, v10> ∈ pInTransit(P.M[P])@i
⊢ (↑x = v9) ⇒ (fst(v7) < t ∨ (∃m:ℕlg-size(S2). (v7 = (fst(lg-label(S2;m))) ∈ (ℤ × Id))))

2
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. S1 : component(P.M[P]) List@i
6. S2 : LabeledDAG(pInTransit(P.M[P]))@i
7. env : pEnvType(P.M[P])@i
8. ∀t:ℕ
let info,Cs,G = pRun(<S1, S2>;env;n2m;l2m) t in

     ∀x∈G.((fst(fst(x))) ≤ t) ∨ (∃m:ℕlg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))) ∈ (ℤ × Id)))

9. <S1, S2> ∈ System(P.M[P])
10. t : {1...}
11. x : Id@i
12. v1 : ℕ@i
13. v3 : ℕ@i
14. v4 : Id@i
15. (env t pRun(<S1, S2>;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
16. v5 : component(P.M[P]) List@i
17. v6 : LabeledDAG(pInTransit(P.M[P]))@i
18. (snd((pRun(<S1, S2>;env;n2m;l2m) (t - 1)))) = <v5, v6> ∈ System(P.M[P])@i
19. ↑null(lg-in-edges(v6;v1))
20. v1 < lg-size(v6)
21. v7 : ℤ × Id@i
22. v9 : Id@i
23. v10 : pCom(P.M[P])@i
24. lg-label(v6;v1) = <v7, v9, v10> ∈ pInTransit(P.M[P])@i
25. (↑x = v9) ⇒ (fst(v7) < t ∨ (∃m:ℕlg-size(S2). (v7 = (fst(lg-label(S2;m))) ∈ (ℤ × Id))))
⊢ (↑let info,S = if com-kind(v10) =a "msg"

                   then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

    if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

    if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

                           then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

            if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>

                            then <inl <v7, v9, comm-msg(v10)>, deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "create" then <inr ⋅ , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))>

             if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))>

             else <inr ⋅ , v5, lg-remove(v6;v1)>
             fi
             in let ev,z,m = outl(info) in
                <ev, m>))
       = (fst(lg-label(S2;m)))
       ∈ (ℤ × Id))))

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. S1 : component(P.M[P]) List@i 6. S2 : LabeledDAG(pInTransit(P.M[P]))@i 7. env : pEnvType(P.M[P])@i 8. \mforall{}t:\mBbbN{} let info,Cs,G = pRun(<S1, S2>env;n2m;l2m) t in \mforall{}x\mmember{}G.((fst(fst(x))) \mleq{} t) \mvee{} (\mexists{}m:\mBbbN{}lg-size(S2). ((fst(x)) = (fst(lg-label(S2;m))))) 9. <S1, S2> \mmember{} System(P.M[P]) 10. t : \{1...\} 11. x : Id@i 12. v1 : \mBbbN{}@i 13. v3 : \mBbbN{}@i 14. v4 : Id@i 15. (env t pRun(<S1, S2>env;n2m;l2m)) = <v1, v3, v4>@i 16. v5 : component(P.M[P]) List@i 17. v6 : LabeledDAG(pInTransit(P.M[P]))@i 18. (snd((pRun(<S1, S2>env;n2m;l2m) (t - 1)))) = <v5, v6>@i 19. \muparrow{}null(lg-in-edges(v6;v1)) 20. v1 < lg-size(v6) 21. v7 : \mBbbZ{} \mtimes{} Id@i 22. v9 : Id@i 23. v10 : pCom(P.M[P])@i 24. lg-label(v6;v1) = <v7, v9, v10>@i \mvdash{} (\muparrow{}let info,S = if com-kind(v10) =a "msg" then <inl <v7, v9, comm-msg(v10)> , deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1)) > if com-kind(v10) =a "create" then <inr \mcdot{} , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1\000C))> else <inr \mcdot{} , v5, lg-remove(v6;v1)> fi in isl(info) \mwedge{}\msubb{} let ev,z,m = outl(info) in x = z) {}\mRightarrow{} (fst(fst(let info,S = if com-kind(v10) =a "msg" then <inl <v7, v9, comm-msg(v10)> , deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1)) > if com-kind(v10) =a "create" then <inr \mcdot{} , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))> else <inr \mcdot{} , v5, lg-remove(v6;v1)> fi in let ev,z,m = outl(info) in <ev, m>)) < t \mvee{} (\mexists{}m:\mBbbN{}lg-size(S2) ((fst(let info,S = if com-kind(v10) =a "msg" then <inl <v7, v9, comm-msg(v10)> , deliver-msg(t;comm-msg(v10);v9;v5;lg-remove(v6;v1)) > if com-kind(v10) =a "create" then <inr \mcdot{} , create-component(t;comm-create(v10);v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "choose" then <inl <v7, v9, n2m v3>, deliver-msg(t;n2m v3;v9;v5;lg-remove(v6;v1))> if com-kind(v10) =a "new" then <inl <v7, v9, l2m v4>, deliver-msg(t;l2m v4;v9;v5;lg-remove(v6;v1))> else <inr \mcdot{} , v5, lg-remove(v6;v1)> fi in let ev,z,m = outl(info) in <ev, m>)) = (fst(lg-label(S2;m)))))) By Latex: Assert \mkleeneopen{}(\muparrow{}x = v9) {}\mRightarrow{} (fst(v7) < t \mvee{} (\mexists{}m:\mBbbN{}lg-size(S2). (v7 = (fst(lg-label(S2;m))))))\mkleeneclose{}\mcdot{} Home Index