---

Step * 1 of Lemma cut-order-iff1


1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. a : E(X)@i
6. b : E(X)@i
⊢ a ∈ cut(X;f;{b})
⇐⇒ (a = b ∈ E(X)) ∨ ((f b < b) ∧ a ∈ cut(X;f;{f b})) ∨ ((↑b ∈b prior(X)) ∧ a ∈ cut(X;f;{prior(X)(b)}))
BY
{ ((RW (AddrC [1;3] (LemmaC `cut-of-singleton`)) 0 THENA Auto)
   THEN Try ((Unfold `label` 0 THEN MemTypeHD (-1) THEN Auto))
   ) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. f : sys-antecedent(es;X)@i
5. a : E(X)@i
6. b : E(X)@i
⊢ a ∈ if b ∈b prior(X) then if f b = b then {b} else {b} ∪ cut(X;f;{f b}) fi  ∪ cut(X;f;{prior(X)(b)})
  if f b = b then {b}
  else {b} ∪ cut(X;f;{f b})
  fi 
⇐⇒ (a = b ∈ E(X)) ∨ ((f b < b) ∧ a ∈ cut(X;f;{f b})) ∨ ((↑b ∈b prior(X)) ∧ a ∈ cut(X;f;{prior(X)(b)}))

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  X  :  EClass(Top)@i'
4.  f  :  sys-antecedent(es;X)@i
5.  a  :  E(X)@i
6.  b  :  E(X)@i
\mvdash{}  a  \mmember{}  cut(X;f;\{b\})
\mLeftarrow{}{}\mRightarrow{}  (a  =  b)  \mvee{}  ((f  b  <  b)  \mwedge{}  a  \mmember{}  cut(X;f;\{f  b\}))  \mvee{}  ((\muparrow{}b  \mmember{}\msubb{}  prior(X))  \mwedge{}  a  \mmember{}  cut(X;f;\{prior(X)(b)\}))


By

---

Latex:
((RW  (AddrC  [1;3]  (LemmaC  `cut-of-singleton`))  0  THENA  Auto)
  THEN  Try  ((Unfold  `label`  0  THEN  MemTypeHD  (-1)  THEN  Auto))
  )

---

Home Index