---

Step * 2 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 ∈ 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)
BY
{ (RepeatFor 2 (GenListD 0)
   THEN SplitOrHyps
   THEN Auto
   THEN Try (Complete ((GenListD 0 THEN OrLeft THEN Auto)))
   THEN SplitOnHypITE (-2)
   THEN Auto
   THEN GenListD 0
   THEN (OrRight THENA Auto)
   THEN GenListD 0
   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{}  L)  \mvee{}  if  (\mexists{}z\mmember{}L.test  x  z)\_b  then  False  else  p  =  x  fi  @i
\mvdash{}  (p  \mmember{}  pv11\_p1\_add\_if\_new()  test  x  L)


By

---

Latex:
(RepeatFor  2  (GenListD  0)
  THEN  SplitOrHyps
  THEN  Auto
  THEN  Try  (Complete  ((GenListD  0  THEN  OrLeft  THEN  Auto)))
  THEN  SplitOnHypITE  (-2)
  THEN  Auto
  THEN  GenListD  0
  THEN  (OrRight  THENA  Auto)
  THEN  GenListD  0
  THEN  Auto)\mcdot{}

---

Home Index