---

Step * of Lemma eo-strict-forward-pred?

∀[Info:Type]. ∀[eo:EO+(Info)]. ∀[e:E].
  ∀e1:E. (es-pred?(eo>e;e1) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else es-pred?(eo;e1) fi  ∈ (E?))
BY
{ (Auto
   THEN (InstLemma `eo-strict-forward-E-subtype` [⌜Info⌝;⌜eo⌝;⌜e⌝]⋅ THENA Auto)
   THEN (InstLemma `es-pred?_property` [⌜eo⌝;⌜e1⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (InstLemma `es-pred?_property` [⌜eo>e⌝;⌜e1⌝]⋅ THENA Auto)
   THEN MoveToConcl (-1)
   THEN (RWW "eo-strict-forward-loc eo-strict-forward-less" 0 THENA Auto)
   THEN GenConclAtAddr [1;1]
   THEN D (-2)
   THEN Reduce 0
   THEN GenConclAtAddr [2;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. x : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
7. es-pred?(eo>e;e1) = (inl x) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
8. x1 : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
9. es-pred?(eo;e1) = (inl x1) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
10. loc(x) = loc(e1) ∈ Id@i
11. (x < e1)@i
12. ∀e':E. (e' < e1) ⇒ ((e' = x ∈ E) ∨ (e' < x)) supposing loc(e') = loc(e1) ∈ Id@i
13. loc(x1) = loc(e1) ∈ Id@i
14. (x1 < e1)@i
15. ∀e':E. (e' < e1) ⇒ ((e' = x1 ∈ E) ∨ (e' < x1)) supposing loc(e') = loc(e1) ∈ Id@i
⊢ (inl x) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else inl x1 fi  ∈ (E?)

2
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. x : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
7. es-pred?(eo>e;e1) = (inl x) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
8. y : Unit@i
9. es-pred?(eo;e1) = (inr y ) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
10. loc(x) = loc(e1) ∈ Id@i
11. (x < e1)@i
12. ∀e':E. (e' < e1) ⇒ ((e' = x ∈ E) ∨ (e' < x)) supposing loc(e') = loc(e1) ∈ Id@i
13. ∀e':E. ¬(e' < e1) supposing loc(e') = loc(e1) ∈ Id@i
⊢ (inl x) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else inr y  fi  ∈ (E?)

3
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. y : Unit@i
7. es-pred?(eo>e;e1) = (inr y ) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
8. x : {e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} @i
9. es-pred?(eo;e1) = (inl x) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
10. ∀e':E. ¬(e' < e1) supposing loc(e') = loc(e1) ∈ Id@i
11. loc(x) = loc(e1) ∈ Id@i
12. (x < e1)@i
13. ∀e':E. (e' < e1) ⇒ ((e' = x ∈ E) ∨ (e' < x)) supposing loc(e') = loc(e1) ∈ Id@i
⊢ (inr y ) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else inl x fi  ∈ (E?)

4
1. Info : Type
2. eo : EO+(Info)
3. e : E
4. e1 : E@i
5. E ⊆r E
6. y : Unit@i
7. es-pred?(eo>e;e1) = (inr y ) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
8. y1 : Unit@i
9. es-pred?(eo;e1) = (inr y1 ) ∈ ({e':E| (e' <loc e1) ∧ (e' = pred(e1) ∈ E)} ?)@i
10. ∀e':E. ¬(e' < e1) supposing loc(e') = loc(e1) ∈ Id@i
11. ∀e':E. ¬(e' < e1) supposing loc(e') = loc(e1) ∈ Id@i
⊢ (inr y ) = if loc(e) = loc(e1) ∧b (es-eq(eo) pred(e1) e) then inr ⋅  else inr y1  fi  ∈ (E?)

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[eo:EO+(Info)].  \mforall{}[e:E].
    \mforall{}e1:E
        (es-pred?(eo>e;e1)
        =  if  loc(e)  =  loc(e1)  \mwedge{}\msubb{}  (es-eq(eo)  pred(e1)  e)  then  inr  \mcdot{}    else  es-pred?(eo;e1)  fi  )


By

---

Latex:
(Auto
  THEN  (InstLemma  `eo-strict-forward-E-subtype`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `es-pred?\_property`  [\mkleeneopen{}eo\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (InstLemma  `es-pred?\_property`  [\mkleeneopen{}eo>e\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (RWW  "eo-strict-forward-loc  eo-strict-forward-less"  0  THENA  Auto)
  THEN  GenConclAtAddr  [1;1]
  THEN  D  (-2)
  THEN  Reduce  0
  THEN  GenConclAtAddr  [2;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index