---

Step * 2 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. r1 ≤ (∃x∈r2.Q[x])_b
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b
BY
{ (Assert ⌜∀z:Top + Top. ((z ∧b Q[x]) ∨br1 ≤ (∃x∈if z then [x / r2] else r2 fi .Q[x])_b)⌝⋅
   THENA ((D 0 THENA Auto) THEN D -1 THEN Reduce 0 THEN Try (Trivial) THEN RWO "bl-exists-cons" 0 THEN Auto)
   ) }

1
1. Q : Base
2. L : Base
3. P : Base
4. x : Base
5. y : Base
6. r1 : Base
7. r2 : Base
8. r1 ≤ (∃x∈r2.Q[x])_b
9. ∀z:Top + Top. ((z ∧b Q[x]) ∨br1 ≤ (∃x∈if z then [x / r2] else r2 fi .Q[x])_b)
⊢ ((P x) ∧b Q[x]) ∨br1 ≤ (∃x∈if P x then [x / r2] else r2 fi .Q[x])_b

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}z:Top  +  Top.  ((z  \mwedge{}\msubb{}  Q[x])  \mvee{}\msubb{}r1  \mleq{}  (\mexists{}x\mmember{}if  z  then  [x  /  r2]  else  r2  fi  .Q[x])\_b)\mkleeneclose{}\mcdot{}
  THENA  ((D  0  THENA  Auto)
                THEN  D  -1
                THEN  Reduce  0
                THEN  Try  (Trivial)
                THEN  RWO  "bl-exists-cons"  0
                THEN  Auto)
  )

---

Home Index