---

Step * 1 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 ∈ 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)}))
BY
{ ((Assert f b c≤ b BY
          (DVar `f'⋅ THEN Unhide⋅ THEN Auto))
   THEN RepeatFor 2 ((SplitOnConclITE THENA Auto))
   THEN Try ((Assert (f b < b) BY (D -3 THEN Complete (Auto))))
   THEN Reduce 0
   THEN ((RWW "member-fset-union" 0 THENM RWW "member-fset-singleton" 0) THENA Auto)
   THEN Try (((Assert ¬(f b < b) BY ((D 0 THENM RelRST) THEN Complete (Auto))) THEN Auto THEN SplitOrHyps THEN Auto))
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN SplitOrHyps
   THEN Auto) }

---

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{}  if  b  \mmember{}\msubb{}  prior(X)
                then  if  f  b  =  b  then  \{b\}  else  \{b\}  \mcup{}  cut(X;f;\{f  b\})  fi    \mcup{}  cut(X;f;\{prior(X)(b)\})
    if  f  b  =  b  then  \{b\}
    else  \{b\}  \mcup{}  cut(X;f;\{f  b\})
    fi 
\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:
((Assert  f  b  c\mleq{}  b  BY
                (DVar  `f'\mcdot{}  THEN  Unhide\mcdot{}  THEN  Auto))
  THEN  RepeatFor  2  ((SplitOnConclITE  THENA  Auto))
  THEN  Try  ((Assert  (f  b  <  b)  BY  (D  -3  THEN  Complete  (Auto))))
  THEN  Reduce  0
  THEN  ((RWW  "member-fset-union"  0  THENM  RWW  "member-fset-singleton"  0)  THENA  Auto)
  THEN  Try  (((Assert  \mneg{}(f  b  <  b)  BY
                                      ((D  0  THENM  RelRST)  THEN  Complete  (Auto)))
                        THEN  Auto
                        THEN  SplitOrHyps
                        THEN  Auto))
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  SplitOrHyps
  THEN  Auto)

---

Home Index