---

Step * of 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 )
BY
{ Auto }

1
1. A : Type@i'
2. p : A@i
3. x : A@i
4. L : A List@i
5. test : A ─→ A ─→ 𝔹@i
6. (p ∈ pv11_p1_add_if_new() test x L)@i
⊢ (p ∈ L) ∨ if (∃z∈L.test x z)_b then False else p = x ∈ A fi 

2
1. A : Type@i'
2. p : A@i
3. x : A@i
4. L : A List@i
5. test : A ─→ A ─→ 𝔹@i
6. (p ∈ L) ∨ if (∃z∈L.test x z)_b then False else p = x ∈ A fi @i
⊢ (p ∈ pv11_p1_add_if_new() test x L)

---

Latex:

---

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  )


By

---

Latex:
Auto

---

Home Index