---

Step * of Lemma chain-pullback

∀[Info:Type]
  ∀es:EO+(Info). ∀Sys:EClass(Top). ∀f:sys-antecedent(es;Sys). ∀b,e:E(Sys).
    (b is f*(e)
    ⇒ ∃e':E(Sys). ((loc(e') = loc(e) ∈ Id) ∧ e' is f*(e) ∧ b is f*(e') ∧ (¬(loc(f e') = loc(e') ∈ Id))) 
       supposing ¬(loc(b) = loc(e) ∈ Id))
BY
{ (RepeatFor 5 ((D 0 THENA Auto)) THEN CausalInd') }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. Sys : EClass(Top)@i'
4. f : sys-antecedent(es;Sys)@i
5. b : E(Sys)@i
6. e : E(Sys)@i
7. ∀e1:E(Sys)
     ((e1 < e)
     ⇒ b is f*(e1)
     ⇒ ∃e':E(Sys). ((loc(e') = loc(e1) ∈ Id) ∧ e' is f*(e1) ∧ b is f*(e') ∧ (¬(loc(f e') = loc(e') ∈ Id))) 
        supposing ¬(loc(b) = loc(e1) ∈ Id))
⊢ b is f*(e)
⇒ ∃e':E(Sys). ((loc(e') = loc(e) ∈ Id) ∧ e' is f*(e) ∧ b is f*(e') ∧ (¬(loc(f e') = loc(e') ∈ Id))) 
   supposing ¬(loc(b) = loc(e) ∈ Id)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}Sys:EClass(Top).  \mforall{}f:sys-antecedent(es;Sys).  \mforall{}b,e:E(Sys).
        (b  is  f*(e)
        {}\mRightarrow{}  \mexists{}e':E(Sys).  ((loc(e')  =  loc(e))  \mwedge{}  e'  is  f*(e)  \mwedge{}  b  is  f*(e')  \mwedge{}  (\mneg{}(loc(f  e')  =  loc(e')))) 
              supposing  \mneg{}(loc(b)  =  loc(e)))


By

---

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

---

Home Index