Nuprl Lemma : pv11_p1_upd_desc_iff

Cmd:ValueAllType. ∀proposals1,proposals2:(ℤ × Cmd) List. ∀s:ℤ. ∀c:Cmd.
  ((<s, c> ∈ pv11_p1_update_proposals(Cmd) proposals1 proposals2)
  ⇐⇒ (<s, c> ∈ proposals2) ∨ ((<s, c> ∈ proposals1) ∧ (∃c':Cmd. (<s, c'> ∈ proposals2)))))


Proof




Definitions occuring in Statement :  pv11_p1_update_proposals: pv11_p1_update_proposals(Cmd) l_member: (x ∈ l) list: List vatype: ValueAllType all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q not: ¬A or: P ∨ Q and: P ∧ Q apply: a pair: <a, b> product: x:A × B[x] int:
Lemmas :  pv11_p1_upd_desc l_member_wf pv11_p1_update_proposals_wf member_append filter_wf5 bnot_wf bl-exists_wf eq_int_wf member_filter_2 iff_transitivity assert_wf not_wf l_exists_wf equal-wf-base-T int_subtype_base iff_weakening_uiff assert_of_bnot l_exists_functionality assert_of_eq_int set_wf assert-bl-exists l_exists_iff subtype_base_sq pair-eta or_wf exists_wf list_wf valueall-type_wf

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}proposals1,proposals2:(\mBbbZ{}  \mtimes{}  Cmd)  List.  \mforall{}s:\mBbbZ{}.  \mforall{}c:Cmd.
    ((<s,  c>  \mmember{}  pv11\_p1\_update\_proposals(Cmd)  proposals1  proposals2)
    \mLeftarrow{}{}\mRightarrow{}  (<s,  c>  \mmember{}  proposals2)  \mvee{}  ((<s,  c>  \mmember{}  proposals1)  \mwedge{}  (\mneg{}(\mexists{}c':Cmd.  (<s,  c'>  \mmember{}  proposals2)))))



Date html generated: 2015_07_23-PM-04_44_54
Last ObjectModification: 2015_01_29-AM-09_53_36

Home Index