### Nuprl Lemma : pv11_p1_add_if_new_iff2

`∀A:Type. ∀p,x:A. ∀L:A List. ∀test:A ─→ A ─→ 𝔹.`
`  ((p ∈ pv11_p1_add_if_new() test x L) `⇐⇒` (p ∈ L) ∨ if (∃z∈L.test x z)_b then False else p = x ∈ A fi )`

Proof

Definitions occuring in Statement :  pv11_p1_add_if_new: `pv11_p1_add_if_new()` bl-exists: `(∃x∈L.P[x])_b` l_member: `(x ∈ l)` list: `T List` ifthenelse: `if b then t else f fi ` bool: `𝔹` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` or: `P ∨ Q` false: `False` apply: `f a` function: `x:A ─→ B[x]` universe: `Type` equal: `s = t ∈ T`
Lemmas :  l_member_wf pv11_p1_add_if_new_wf bool_wf list_wf or_wf bl-exists_wf eqtt_to_assert assert-bl-exists false_wf eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot l_exists_wf assert_wf bool_cases iff_transitivity bnot_wf not_wf iff_weakening_uiff assert_of_bnot member_append cons_wf nil_wf member_singleton equal-wf-T-base cons_member

Latex:
\mforall{}A:Type.  \mforall{}p,x:A.  \mforall{}L:A  List.  \mforall{}test:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}.
((p  \mmember{}  pv11\_p1\_add\_if\_new()  test  x  L)  \mLeftarrow{}{}\mRightarrow{}  (p  \mmember{}  L)  \mvee{}  if  (\mexists{}z\mmember{}L.test  x  z)\_b  then  False  else  p  =  x  fi  )

Date html generated: 2015_07_23-PM-04_44_30
Last ObjectModification: 2015_01_29-AM-11_20_46

Home Index