---

Step * 1 1 of Lemma cut-of-singleton


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))
BY
{ (((InstLemma `cut-of-property` [Info; ⌈es⌉;⌈X⌉;⌈f⌉]⋅ THENM InstHyp [⌈{f e}⌉] (-1)⋅ THENM InstHyp [⌈{e}⌉] (-2)⋅)
    THENA Try (Complete (Auto))
    )
   THEN RepeatFor 2 (OldAutoSplit)
   ) }

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
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c')
8. {e} ⊆ cut(X;f;{e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c')
9. ↑e ∈b prior(X)
10. (f e) = e ∈ E
⊢ cut(X;f;{e}) = {e} ∪ cut(X;f;{prior(X)(e)}) ∈ fset(E(X))

2
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
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c')
8. {e} ⊆ cut(X;f;{e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c')
9. ↑e ∈b prior(X)
10. ¬((f e) = e ∈ E)
⊢ cut(X;f;{e}) = {e} ∪ cut(X;f;{f e}) ∪ cut(X;f;{prior(X)(e)}) ∈ fset(E(X))

3
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
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c')
8. {e} ⊆ cut(X;f;{e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c')
9. ¬↑e ∈b prior(X)
10. (f e) = e ∈ E
⊢ cut(X;f;{e}) = {e} ∈ fset(E(X))

4
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
6. ∀[s:fset(E(X))]. (s ⊆ cut(X;f;s) ∧ (∀[c':Cut(X;f)]. cut(X;f;s) ⊆ c' supposing s ⊆ c'))
7. {f e} ⊆ cut(X;f;{f e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{f e}) ⊆ c' supposing {f e} ⊆ c')
8. {e} ⊆ cut(X;f;{e}) ∧ (∀[c':Cut(X;f)]. cut(X;f;{e}) ⊆ c' supposing {e} ⊆ c')
9. ¬↑e ∈b prior(X)
10. ¬((f e) = e ∈ E)
⊢ cut(X;f;{e}) = {e} ∪ cut(X;f;{f e}) ∈ fset(E(X))

---

Latex:

---

Latex:

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
\mvdash{}  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:
(((InstLemma  `cut-of-property`  [Info;  \mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
      THENM  InstHyp  [\mkleeneopen{}\{f  e\}\mkleeneclose{}]  (-1)\mcdot{}
      THENM  InstHyp  [\mkleeneopen{}\{e\}\mkleeneclose{}]  (-2)\mcdot{})
    THENA  Try  (Complete  (Auto))
    )
  THEN  RepeatFor  2  (OldAutoSplit)
  )

---

Home Index