Proof of Nuprl Lemma : local-simulation-validity

Step * 1 1 1 1 1 1 of Lemma local-simulation-validity

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. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ (∀e:E. ∀v:Interface.  (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. e' < ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))||
23. R[v;info(e')]
24. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
25. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
26. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
27. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
⊢ (snd(msg-body(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']))))
= (snd(local-simulation-inputs(es;e;hdr;locs)[e']))
∈ Message(g)
BY
{ (RepUR ``local-simulation-inputs mapfilter es-le-before`` 0
   THEN (RWW "map_append_sq filter_append_sq filter-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN MoveToConcl (-6)
   THEN GenConcl ⌈filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))
                  = L
                  ∈ ({e:E| msg-header(info(e)) = hdr ∈ Name}  List)⌉⋅) }

1
.....wf.....
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. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ (∀e:E. ∀v:Interface.  (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)

⊢ filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) ∈ {e:E| msg-header(info(e)) = hdr ∈ Name}  List

2
.....wf.....
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. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ (∀e:E. ∀v:Interface.  (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
⊢ {e:E| msg-header(info(e)) = hdr ∈ Name}  List ∈ Type

3
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. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ (∀e:E. ∀v:Interface.  (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
27. L : {e:E| msg-header(info(e)) = hdr ∈ Name}  List@i

28. filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) = L ∈ ({e:E| msg-header(info(e)) = hdr ∈ Name}  List)@\000Ci

⊢ e' < ||L||
⇒ ((snd(msg-body(info(L[e']))))
= (snd(map(λm.msg-body(m);map(λe.info(e);L))

     @ map(λm.msg-body(m);map(λe.info(e);if has-header-and-in-locs(info(e);hdr;locs) then [e] else [] fi ))[e']))

∈ Message(g))

Latex:

Latex:
1. correct : Id {}\mrightarrow{} \mBbbP{}@i' 2. g : Name {}\mrightarrow{} Type@i' 3. f : Name {}\mrightarrow{} Type@i' 4. X : EClass(Interface)@i' 5. LocalClass(X)@i' 6. locs : bag(Id)@i 7. hdr : Name@i 8. hdr encodes Id \mtimes{} Message(g) 9. hdrs : Name List@i 10. es : EO+(Message(f))@i' 11. \mforall{}i:Id. ((correct i) {}\mRightarrow{} local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i 12. P : Interface {}\mrightarrow{} \mBbbP{}@i' 13. R : Interface {}\mrightarrow{} Message(g) {}\mrightarrow{} \mBbbP{}@i' 14. \mforall{}eo:EO+(Message(g)) (eo-msg-interface-constraint(eo;X;hdrs;g) {}\mRightarrow{} (\mforall{}e:E. \mforall{}v:Interface. (v \mmember{} X(e) {}\mRightarrow{} P[v] {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} R[v;info(e')])))))@i' 15. e : E@i 16. v : Interface@i 17. correct loc(e)@i 18. \muparrow{}has-header-and-in-locs(info(e);hdr;locs) 19. v \mmember{} X(local-simulation-event(es;e;hdr;locs)) 20. P[v]@i 21. e' : \{e:\mBbbN{}||local-simulation-inputs(es;e;hdr;locs)||| True\} 22. e' < ||filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))|| 23. R[v;info(e')] 24. (filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e) 25. \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs); before(e))[e']);hdr;locs) 26. (filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e) 27. \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs); before(e))[e']);hdr;locs) \mvdash{} (snd(msg-body(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'])))) = (snd(local-simulation-inputs(es;e;hdr;locs)[e'])) By Latex: (RepUR ``local-simulation-inputs mapfilter es-le-before`` 0 THEN (RWW "map\_append\_sq filter\_append\_sq filter-map" 0 THENA Auto) THEN RepUR ``compose`` 0 THEN MoveToConcl (-6) THEN GenConcl \mkleeneopen{}filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e)) = L\mkleeneclose{}\mcdot{}) Home Index