---

Step * 1 of Lemma pv11_p1_add_if_new_iff2


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 
BY
{ (RepeatFor 2 (GenListD (-1))
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN GenListD (-1)
   THEN D (-1)
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN GenListD (-1)
   THEN AutoSplit
   THEN OrRight
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type@i'
2.  p  :  A@i
3.  x  :  A@i
4.  L  :  A  List@i
5.  test  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}@i
6.  (p  \mmember{}  pv11\_p1\_add\_if\_new()  test  x  L)@i
\mvdash{}  (p  \mmember{}  L)  \mvee{}  if  (\mexists{}z\mmember{}L.test  x  z)\_b  then  False  else  p  =  x  fi 


By

---

Latex:
(RepeatFor  2  (GenListD  (-1))
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  GenListD  (-1)
  THEN  D  (-1)
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  GenListD  (-1)
  THEN  AutoSplit
  THEN  OrRight
  THEN  Auto)\mcdot{}

---

Home Index