---

Step * of Lemma decidable__path-goes-thru

∀[Info:Type]. ∀es:EO+(Info). ∀Sys:EClass(Top). ∀f:sys-antecedent(es;Sys). ∀y,x:E(Sys). ∀i:Id.  Dec(x-f*-y thru i)
BY
{ (RepeatFor 4 ((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. y : E(Sys)@i
6. ∀y1:E(Sys). ((y1 < y) ⇒ (∀x:E(Sys). ∀i:Id.  Dec(x-f*-y1 thru i)))
⊢ ∀x:E(Sys). ∀i:Id.  Dec(x-f*-y thru i)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}Sys:EClass(Top).  \mforall{}f:sys-antecedent(es;Sys).  \mforall{}y,x:E(Sys).  \mforall{}i:Id.
        Dec(x-f*-y  thru  i)


By

---

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

---

Home Index