---

Step * of Lemma cut-of-singleton

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[e:E(X)].
  (cut(X;f;{e})
  = if e ∈b prior(X) then if f e = e then {e} else {e} ∪ cut(X;f;{f e}) fi  ∪ cut(X;f;{prior(X)(e)})
    if f e = e then {e}
    else {e} ∪ cut(X;f;{f e})
    fi 
  ∈ Cut(X;f))
BY
{ RemoveUniform Auto Auto }

1
∀Info:Type. ∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀e:E(X).
  (cut(X;f;{e})
  = if e ∈b prior(X) then if f e = e then {e} else {e} ∪ cut(X;f;{f e}) fi  ∪ cut(X;f;{prior(X)(e)})
    if f e = e then {e}
    else {e} ∪ cut(X;f;{f e})
    fi 
  ∈ Cut(X;f))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[e:E(X)].
    (cut(X;f;\{e\})
    =  if  e  \mmember{}\msubb{}  prior(X)  then  if  f  e  =  e  then  \{e\}  else  \{e\}  \mcup{}  cut(X;f;\{f  e\})  fi    \mcup{}  cut(X;f;\{prior(X)(e)\})
        if  f  e  =  e  then  \{e\}
        else  \{e\}  \mcup{}  cut(X;f;\{f  e\})
        fi  )


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index