---

Step * 2 1 of Lemma pv11_p1_upd_left


1. Cmd : {T:Type| valueall-type(T)} @i'
2. proposals1 : (ℤ × Cmd) List@i
3. proposals2 : (ℤ × Cmd) List@i
4. s : ℤ@i
5. c : Cmd@i
6. (<s, c> ∈ proposals1)@i
7. (<s, c> ∈ proposals1)
8. ∃c':Cmd. (<s, c'> ∈ proposals2)@i
⊢ ∃z:ℤ × Cmd. ((z ∈ proposals2) ∧ (s = (fst(z)) ∈ ℤ))
BY
{ (ExRepD THEN InstConcl [⌈<s, c'>⌉]⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  proposals1  :  (\mBbbZ{}  \mtimes{}  Cmd)  List@i
3.  proposals2  :  (\mBbbZ{}  \mtimes{}  Cmd)  List@i
4.  s  :  \mBbbZ{}@i
5.  c  :  Cmd@i
6.  (<s,  c>  \mmember{}  proposals1)@i
7.  (<s,  c>  \mmember{}  proposals1)
8.  \mexists{}c':Cmd.  (<s,  c'>  \mmember{}  proposals2)@i
\mvdash{}  \mexists{}z:\mBbbZ{}  \mtimes{}  Cmd.  ((z  \mmember{}  proposals2)  \mwedge{}  (s  =  (fst(z))))


By

---

Latex:
(ExRepD  THEN  InstConcl  [\mkleeneopen{}<s,  c'>\mkleeneclose{}]\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index