---

Step * 1 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
{ (Auto THEN MemTypeCD THEN Auto) }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
⊢ 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 
∈ fset(E(X))

2
.....set predicate..... 
1. Info : Type@i'
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. e : E(X)@i
⊢ (cut(X;f;{e}) closed under [f; X-pred])

---

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:
(Auto  THEN  MemTypeCD  THEN  Auto)

---

Home Index