---

Step * 1 of Lemma es-interface-predecessors-step-sq


∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀e:E.
  (≤(X)(e) ~ if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi )
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN CausalInd') }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. e : E@i
5. ∀e1:E
     ((e1 < e) ⇒ (≤(X)(e1) ~ if e1 ∈b prior(X) then ≤(X)(prior(X)(e1)) else [] fi  @ if e1 ∈b X then [e1] else [] fi ))
⊢ ≤(X)(e) ~ if e ∈b prior(X) then ≤(X)(prior(X)(e)) else [] fi  @ if e ∈b X then [e] else [] fi 

---

Latex:

---

Latex:

\mforall{}Info:Type.  \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).  \mforall{}e:E.
    (\mleq{}(X)(e)  \msim{}  if  e  \mmember{}\msubb{}  prior(X)  then  \mleq{}(X)(prior(X)(e))  else  []  fi    @  if  e  \mmember{}\msubb{}  X  then  [e]  else  []  fi  )


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  CausalInd')

---

Home Index