---

Step * 2 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. ((z ∈ proposals2) ∧ (s = (fst(z)) ∈ ℤ)))
⊢ ∃c':Cmd. (<s, c'> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)
BY
{ ((InstConcl [⌈c⌉]⋅ THENA Auto)
   THEN (BLemma `pv11_p1_upd_desc_iff` THENA Auto)
   THEN OrRight
   THEN Auto
   THEN ParallelOp -2
   THEN Auto) }

1
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)) ∈ ℤ))

---

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.  \mneg{}(\mexists{}z:\mBbbZ{}  \mtimes{}  Cmd.  ((z  \mmember{}  proposals2)  \mwedge{}  (s  =  (fst(z)))))
\mvdash{}  \mexists{}c':Cmd.  (<s,  c'>  \mmember{}  pv11\_p1\_update\_proposals(Cmd)  proposals1  proposals2)


By

---

Latex:
((InstConcl  [\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (BLemma  `pv11\_p1\_upd\_desc\_iff`  THENA  Auto)
  THEN  OrRight
  THEN  Auto
  THEN  ParallelOp  -2
  THEN  Auto)

---

Home Index