---

Step * of Lemma es-cut-add-at

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top)]. ∀[f:sys-antecedent(es;X)]. ∀[c:Cut(X;f)]. ∀[e:E(X)].
  ((c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List))
     ∧ (c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List))
     ∧ (∀[i:Id]. c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id}  List) supposing ¬(i = loc(e) ∈ Id))) supposing 
     ((¬e ∈ c) and 
     ((↑e ∈b prior(X)) ⇒ prior(X)(e) ∈ c) and 
     ((¬((f e) = e ∈ E(X))) ⇒ f e ∈ c))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert c+e ∈ Cut(X;f) BY
               Auto)
   THEN (Assert c+e ∈ fset(E) BY
               ((DoSubsume THEN Auto) THEN D 0 THEN Auto THEN D (-1) THEN Auto))
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. c : Cut(X;f)
6. e : E(X)
7. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c
8. (↑e ∈b prior(X)) ⇒ prior(X)(e) ∈ c
9. ¬e ∈ c
10. c+e ∈ Cut(X;f)
11. c+e ∈ fset(E)
⊢ c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List)

2
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. c : Cut(X;f)
6. e : E(X)
7. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c
8. (↑e ∈b prior(X)) ⇒ prior(X)(e) ∈ c
9. ¬e ∈ c
10. c+e ∈ Cut(X;f)
11. c+e ∈ fset(E)
12. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List)
⊢ c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List)

3
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. f : sys-antecedent(es;X)
5. c : Cut(X;f)
6. e : E(X)
7. (¬((f e) = e ∈ E(X))) ⇒ f e ∈ c
8. (↑e ∈b prior(X)) ⇒ prior(X)(e) ∈ c
9. ¬e ∈ c
10. c+e ∈ Cut(X;f)
11. c+e ∈ fset(E)
12. c+e(loc(e)) = (c(loc(e)) @ [e]) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List)
13. c+e(loc(e)) = ≤(X)(e) ∈ ({e':E(X)| loc(e') = loc(e) ∈ Id}  List)
14. i : Id
15. ¬(i = loc(e) ∈ Id)
⊢ c+e(i) = c(i) ∈ ({e:E(X)| loc(e) = i ∈ Id}  List)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top)].  \mforall{}[f:sys-antecedent(es;X)].  \mforall{}[c:Cut(X;f)].
\mforall{}[e:E(X)].
    ((c+e(loc(e))  =  (c(loc(e))  @  [e]))
          \mwedge{}  (c+e(loc(e))  =  \mleq{}(X)(e))
          \mwedge{}  (\mforall{}[i:Id].  c+e(i)  =  c(i)  supposing  \mneg{}(i  =  loc(e))))  supposing 
          ((\mneg{}e  \mmember{}  c)  and 
          ((\muparrow{}e  \mmember{}\msubb{}  prior(X))  {}\mRightarrow{}  prior(X)(e)  \mmember{}  c)  and 
          ((\mneg{}((f  e)  =  e))  {}\mRightarrow{}  f  e  \mmember{}  c))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  c+e  \mmember{}  Cut(X;f)  BY
                          Auto)
  THEN  (Assert  c+e  \mmember{}  fset(E)  BY
                          ((DoSubsume  THEN  Auto)  THEN  D  0  THEN  Auto  THEN  D  (-1)  THEN  Auto))
  THEN  Auto)

---

Home Index