---

Step * 1 of Lemma es-prior-interface-val-pred


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
⊢ prior(X)(e) = if pred(e) ∈b X then pred(e) else prior(X)(pred(e)) fi  ∈ E
BY
{ ((DupHyp (-1) THEN (RWO "es-is-prior-interface-pred" (-1) THENA Auto)) THEN (SplitOnConclITE THENA Auto)) }

1
.....truecase..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
6. (¬↑first(e)) ∧ ((↑pred(e) ∈b X) ∨ (↑pred(e) ∈b prior(X)))
7. ↑pred(e) ∈b X
⊢ prior(X)(e) = pred(e) ∈ E

2
.....falsecase..... 
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. e : E
5. ↑e ∈b prior(X)
6. (¬↑first(e)) ∧ ((↑pred(e) ∈b X) ∨ (↑pred(e) ∈b prior(X)))
7. ¬↑pred(e) ∈b X
⊢ prior(X)(e) = prior(X)(pred(e)) ∈ E

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  e  :  E
5.  \muparrow{}e  \mmember{}\msubb{}  prior(X)
\mvdash{}  prior(X)(e)  =  if  pred(e)  \mmember{}\msubb{}  X  then  pred(e)  else  prior(X)(pred(e))  fi 


By

---

Latex:
((DupHyp  (-1)  THEN  (RWO  "es-is-prior-interface-pred"  (-1)  THENA  Auto))
  THEN  (SplitOnConclITE  THENA  Auto)
  )

---

Home Index