---

Step * 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. z : ℤ × Cmd
8. (z ∈ proposals2)
9. s = (fst(z)) ∈ ℤ
⊢ ∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)
BY
{ ((InstConcl [⌈snd(z)⌉]⋅ THENA Auto)
   THEN BLemma `pv11_p1_upd_desc_iff`
   THEN Auto
   THEN OrLeft
   THEN Auto
   THEN HypSubst' (-1) 0
   THEN RWO "pair-eta<" 0
   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.  z  :  \mBbbZ{}  \mtimes{}  Cmd
8.  (z  \mmember{}  proposals2)
9.  s  =  (fst(z))
\mvdash{}  \mexists{}c':Cmd.  (<s,  c'>  \mmember{}  pv11\_p1\_update\_proposals(Cmd)  proposals1  proposals2)


By

---

Latex:
((InstConcl  [\mkleeneopen{}snd(z)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BLemma  `pv11\_p1\_upd\_desc\_iff`
  THEN  Auto
  THEN  OrLeft
  THEN  Auto
  THEN  HypSubst'  (-1)  0
  THEN  RWO  "pair-eta<"  0
  THEN  Auto)

---

Home Index