---

Step * 1 of Lemma filter-interface-predecessors-lower-bound2


1. Info : Type
2. es : EO+(Info)@i'
3. T : Type
4. X : EClass(T)@i'
5. P : E(X) ─→ 𝔹@i
6. ∀e1,e2:E(X).  (loc(e1) = loc(e2) ∈ Id) supposing ((↑P[e2]) and (↑P[e1]))
7. R : Id ─→ E(X) ─→ ℙ
8. ∀x1,x2:Id. ∀y:E(X).  (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ Id))
9. L : Id List@i
10. no_repeats(Id;L)
11. 0 < ||L||
12. (∀x∈L.∃y:E(X). (R[x;y] ∧ (↑P[y])))@i
13. f : ℕ||L|| ─→ {y:E(X)| ↑P[y]} 
14. Inj(ℕ||L||;{y:E(X)| ↑P[y]} ;f)
15. i : ℕ||L||@i
16. j : ℕ||L||@i
⊢ loc(f i) = loc(f j) ∈ Id
BY
{ ((Assert (↑P[f i]) ∧ (↑P[f j]) BY (Auto THEN GenConclAtAddr [1;2] THEN Auto))⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)@i'
3.  T  :  Type
4.  X  :  EClass(T)@i'
5.  P  :  E(X)  {}\mrightarrow{}  \mBbbB{}@i
6.  \mforall{}e1,e2:E(X).    (loc(e1)  =  loc(e2))  supposing  ((\muparrow{}P[e2])  and  (\muparrow{}P[e1]))
7.  R  :  Id  {}\mrightarrow{}  E(X)  {}\mrightarrow{}  \mBbbP{}
8.  \mforall{}x1,x2:Id.  \mforall{}y:E(X).    (R[x1;y]  {}\mRightarrow{}  R[x2;y]  {}\mRightarrow{}  (x1  =  x2))
9.  L  :  Id  List@i
10.  no\_repeats(Id;L)
11.  0  <  ||L||
12.  (\mforall{}x\mmember{}L.\mexists{}y:E(X).  (R[x;y]  \mwedge{}  (\muparrow{}P[y])))@i
13.  f  :  \mBbbN{}||L||  {}\mrightarrow{}  \{y:E(X)|  \muparrow{}P[y]\} 
14.  Inj(\mBbbN{}||L||;\{y:E(X)|  \muparrow{}P[y]\}  ;f)
15.  i  :  \mBbbN{}||L||@i
16.  j  :  \mBbbN{}||L||@i
\mvdash{}  loc(f  i)  =  loc(f  j)


By

---

Latex:
((Assert  (\muparrow{}P[f  i])  \mwedge{}  (\muparrow{}P[f  j])  BY  (Auto  THEN  GenConclAtAddr  [1;2]  THEN  Auto))\mcdot{}  THEN  Auto)

---

Home Index