---

Step * of Lemma es-pred-cle

∀es:EO. ∀e:es-base-E(es).  ((pred(e) < e) ∨ (pred(e) = e ∈ es-base-E(es)))
BY
{ ((D 0 THENA Auto)
   THEN (((InstLemma `es-causl-wf-base` [⌈es⌉]⋅ THENA Auto)
          THEN (InstLemma `es-eq-E-wf-base` [⌈es⌉]⋅ THENA Auto)
          THEN (InstLemma `es-pred-wf-base` [⌈es⌉]⋅ THENA Auto))
         THEN StrongCausalIndAux (ioid Obid: es-causl-swellfnd-base)⋅
         THEN (RecUnfold `es-pred` 0
               THEN Unfold `let` 0
               THEN Reduce 0
               THEN Fold `es-eq-E` 0
               THEN Assert ⌈(pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))⌉⋅)⋅)⋅
   ) }

1
.....assertion..... 
1. es : EO@i'
2. ∀[e,e':es-base-E(es)].  ((e < e') ∈ ℙ)
3. ∀[e,e':es-base-E(es)].  (e = e' ∈ 𝔹)
4. ∀[e:es-base-E(es)]. (pred(e) ∈ es-base-E(es))
5. e : es-base-E(es)@i
6. ∀e1:es-base-E(es). ((e1 < e) ⇒ ((pred(e1) < e1) ∨ (pred(e1) = e1 ∈ es-base-E(es))))
⊢ (pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))

2
1. es : EO@i'
2. ∀[e,e':es-base-E(es)].  ((e < e') ∈ ℙ)
3. ∀[e,e':es-base-E(es)].  (e = e' ∈ 𝔹)
4. ∀[e:es-base-E(es)]. (pred(e) ∈ es-base-E(es))
5. e : es-base-E(es)@i
6. ∀e1:es-base-E(es). ((e1 < e) ⇒ ((pred(e1) < e1) ∨ (pred(e1) = e1 ∈ es-base-E(es))))
7. (pred1(e) < e) ∨ (pred1(e) = e ∈ es-base-E(es))
⊢ (if es-dom(es) pred1(e) then pred1(e)
if pred1(e) = e then e
else pred(pred1(e))
fi  < e)
∨ (if es-dom(es) pred1(e) then pred1(e) if pred1(e) = e then e else pred(pred1(e)) fi  = e ∈ es-base-E(es))

---

Latex:


\mforall{}es:EO.  \mforall{}e:es-base-E(es).    ((pred(e)  <  e)  \mvee{}  (pred(e)  =  e))


By

((D  0  THENA  Auto)
  THEN  (((InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `es-eq-E-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `es-pred-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THENA  Auto))
              THEN  StrongCausalIndAux  (ioid  Obid:  es-causl-swellfnd-base)\mcdot{}
              THEN  (RecUnfold  `es-pred`  0
                          THEN  Unfold  `let`  0
                          THEN  Reduce  0
                          THEN  Fold  `es-eq-E`  0
                          THEN  Assert  \mkleeneopen{}(pred1(e)  <  e)  \mvee{}  (pred1(e)  =  e)\mkleeneclose{}\mcdot{})\mcdot{})\mcdot{}
  )

---

Home Index