---

Step * 1 of Lemma bl-exists-filter


1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. (∃x∈r1.Q[x])_b ≤ r2
⊢ (∃x∈if P x then [x / r1] else r1 fi .Q[x])_b ≤ ((P x) ∧b Q[x]) ∨br2
BY
{ (SqReasoning
   THEN Try ((RWO "bl-exists-cons" 0 THEN Auto))
   THEN Try ((Thin (-1) THEN ComputeSameException 100))
   THEN RepUR ``bl-exists reduce`` -1
   THEN RecUnfold `list_ind` (-1)
   THEN RepeatFor 2 (HasValueD (-1))
   THEN (GenConclTerm ⌜P x⌝⋅ THENA Auto)
   THEN D -2
   THEN Reduce 0
   THEN Try (Trivial)
   THEN RWO "bl-exists-cons" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  Q  :  Base
2.  L  :  Base
3.  P  :  Base
4.  x  :  Base
5.  y  :  Base
6.  r1  :  Base
7.  r2  :  Base
8.  (\mexists{}x\mmember{}r1.Q[x])\_b  \mleq{}  r2
\mvdash{}  (\mexists{}x\mmember{}if  P  x  then  [x  /  r1]  else  r1  fi  .Q[x])\_b  \mleq{}  ((P  x)  \mwedge{}\msubb{}  Q[x])  \mvee{}\msubb{}r2


By

---

Latex:
(SqReasoning
  THEN  Try  ((RWO  "bl-exists-cons"  0  THEN  Auto))
  THEN  Try  ((Thin  (-1)  THEN  ComputeSameException  100))
  THEN  RepUR  ``bl-exists  reduce``  -1
  THEN  RecUnfold  `list\_ind`  (-1)
  THEN  RepeatFor  2  (HasValueD  (-1))
  THEN  (GenConclTerm  \mkleeneopen{}P  x\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  RWO  "bl-exists-cons"  0
  THEN  Auto)

---

Home Index