Proof of Nuprl Lemma : local-simulation-agreement

Step * of Lemma local-simulation-agreement

∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀R:Interface ⟶ Interface ⟶ ℙ. ∀es:EO+(Message(f)).
          ((∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j)))
          ⇒ (∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2]))
          ⇒ any v1,v2 from local-simulation-class(X;locs;hdr) satisfy
             R[v1;v2]
             at locations i.correct i)
        supposing hdr encodes Id × Message(g)))
BY
{ ((Intro⋅ THEN InstLemma `consistent-local-simulation` [])
   THEN RepeatFor 7 ((ParallelLast' THENA Auto))
   THEN RepeatFor 2 (Intro)
   THEN ParallelOp -3
   THEN Thin (-5)

   THEN (InstLemma `local-simulation-inputs_wf` [⌜f⌝;⌜Message(g)⌝;⌜es⌝;⌜hdr⌝;⌜locs⌝]⋅ THENA Auto)

   THEN (Auto THEN D 0 THEN Auto)
   THEN (InstHyp [⌜[e1; e2]⌝] 12⋅
         THENA (Auto
                THEN RWO "pairwise-cons" 0
                THEN Auto
                THEN (FHyp 14 [-7;-6] THENA Auto)
                THEN BackThruHyp' (-1)
                THEN Auto)
         )
   THEN (InstHyp [⌜hdrs⌝] (-1)⋅ THENA Auto)) }

1
.....antecedent.....
1. correct : Id ⟶ ℙ@i'
2. g : Name ⟶ Type@i'
3. f : Name ⟶ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. R : Interface ⟶ Interface ⟶ ℙ@i'
11. es : EO+(Message(f))@i'
12. ∀ee:E List
      ((∀e1,e2∈ee.  local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
      ⇒ (∀hdrs:Name List
            ((∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
            ⇒ (∃eo:EO+(Message(g))
                 (eo-msg-interface-constraint(eo;X;hdrs;g)
                 ∧ (∀e∈ee.∀[v:Interface]

                            (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))

                            supposing v ∈ local-simulation-class(X;locs;hdr)(e)))))))
13. ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Message(g)) List)
14. ∀i,j:Id.  ((correct i) ⇒ (correct j) ⇒ local-simulation-input-consistency(g;X;hdr;locs;es;i;j))@i
15. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
16. ∀eo:EO+(Message(g)). (eo-msg-interface-constraint(eo;X;hdrs;g) ⇒ any v1,v2 from X satisfy R[v1;v2])@i'
17. e1 : E@i
18. e2 : E@i
19. correct loc(e1)@i
20. correct loc(e2)@i
21. v1 : Interface@i
22. v2 : Interface@i
23. v1 ∈ local-simulation-class(X;locs;hdr)(e1)@i
24. v2 ∈ local-simulation-class(X;locs;hdr)(e2)@i
25. ∀hdrs:Name List
      ((∀e∈[e1; e2].eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
      ⇒ (∃eo:EO+(Message(g))
           (eo-msg-interface-constraint(eo;X;hdrs;g)
           ∧ (∀e∈[e1; e2].∀[v:Interface]

                            (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))

                            supposing v ∈ local-simulation-class(X;locs;hdr)(e)))))
⊢ (∀e∈[e1; e2].eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))

2
1. correct : Id ⟶ ℙ@i'
2. g : Name ⟶ Type@i'
3. f : Name ⟶ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. R : Interface ⟶ Interface ⟶ ℙ@i'
11. es : EO+(Message(f))@i'
12. ∀ee:E List
      ((∀e1,e2∈ee.  local-simulation-inputs(es;e1;hdr;locs) || local-simulation-inputs(es;e2;hdr;locs))
      ⇒ (∀hdrs:Name List
            ((∀e∈ee.eo-msg-interface-constraint(local-simulation-eo(es;e;hdr;locs);X;hdrs;g))
            ⇒ (∃eo:EO+(Message(g))
                 (eo-msg-interface-constraint(eo;X;hdrs;g)
                 ∧ (∀e∈ee.∀[v:Interface]

                            (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))

                            (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))

                            supposing v ∈ local-simulation-class(X;locs;hdr)(e)))))
26. ∃eo:EO+(Message(g))
     (eo-msg-interface-constraint(eo;X;hdrs;g)
     ∧ (∀e∈[e1; e2].∀[v:Interface]

                      (↑has-header-and-in-locs(info(e);hdr;locs)) ∧ (∃e':E. v ∈ X(e'))

supposing v ∈ local-simulation-class(X;locs;hdr)(e)))
⊢ R[v1;v2]

Latex:

Latex:
\mforall{}correct:Id {}\mrightarrow{} \mBbbP{}. \mforall{}g,f:Name {}\mrightarrow{} Type. \mforall{}X:EClass(Interface). (LocalClass(X) {}\mRightarrow{} (\mforall{}locs:bag(Id). \mforall{}hdr:Name. \mforall{}hdrs:Name List. \mforall{}R:Interface {}\mrightarrow{} Interface {}\mrightarrow{} \mBbbP{}. \mforall{}es:EO+(Message(f)). ((\mforall{}i,j:Id. ((correct i) {}\mRightarrow{} (correct j) {}\mRightarrow{} local-simulation-input-consistency(g;X;hdr;locs;es;i;j))) {}\mRightarrow{} (\mforall{}i:Id. ((correct i) {}\mRightarrow{} local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))) {}\mRightarrow{} (\mforall{}eo:EO+(Message(g)) (eo-msg-interface-constraint(eo;X;hdrs;g) {}\mRightarrow{} any v1,v2 from X satisfy R[v1;v2])) {}\mRightarrow{} any v1,v2 from local-simulation-class(X;locs;hdr) satisfy R[v1;v2] at locations i.correct i) supposing hdr encodes Id \mtimes{} Message(g))) By Latex: ((Intro\mcdot{} THEN InstLemma `consistent-local-simulation` []) THEN RepeatFor 7 ((ParallelLast' THENA Auto)) THEN RepeatFor 2 (Intro) THEN ParallelOp -3 THEN Thin (-5) THEN (InstLemma `local-simulation-inputs\_wf` [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}Message(g)\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}hdr\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{}]\mcdot{} THENA Auto) THEN (Auto THEN D 0 THEN Auto) THEN (InstHyp [\mkleeneopen{}[e1; e2]\mkleeneclose{}] 12\mcdot{} THENA (Auto THEN RWO "pairwise-cons" 0 THEN Auto THEN (FHyp 14 [-7;-6] THENA Auto) THEN BackThruHyp' (-1) THEN Auto) ) THEN (InstHyp [\mkleeneopen{}hdrs\mkleeneclose{}] (-1)\mcdot{} THENA Auto)) Home Index