---

Step * of Lemma es-local-prior-state-induction

∀[Info,T:Type]. ∀[P:T ─→ ℙ].
  ∀es:EO+(Info)
    ∀[A:Type]
      ∀X:EClass(A). ∀base:T. ∀f:T ─→ A ─→ T. ∀e:E.
        (P[base] ⇒ (∀x:T. ∀e':E(X).  ((e' <loc e) ⇒ P[x] ⇒ P[f x X(e')])) ⇒ P[prior-state(f;base;X;e)])
BY
{ ((LocLessInd THEN Auto) THEN RecUnfold `es-local-prior-state` 0 THEN SplitOnConclITE THEN Auto) }

1
.....truecase..... 
1. [Info] : Type
2. [T] : Type
3. [P] : T ─→ ℙ
4. es : EO+(Info)@i'
5. [A] : Type
6. X : EClass(A)@i'
7. base : T@i
8. f : T ─→ A ─→ T@i
9. WellFnd{i}(E;x,y.(x <loc y))
10. j : E@i
11. ∀k:E
      ((k <loc j)
      ⇒ P[base]
      ⇒ (∀x:T. ∀e':E(X).  ((e' <loc k) ⇒ P[x] ⇒ P[f x X(e')]))
      ⇒ P[prior-state(f;base;X;k)])@i
12. P[base]@i
13. ∀x:T. ∀e':E(X).  ((e' <loc j) ⇒ P[x] ⇒ P[f x X(e')])@i
14. ↑j ∈b prior(X)
⊢ P[f prior-state(f;base;X;prior(X)(j)) X(prior(X)(j))]

---

Latex:

---

Latex:
\mforall{}[Info,T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type]
            \mforall{}X:EClass(A).  \mforall{}base:T.  \mforall{}f:T  {}\mrightarrow{}  A  {}\mrightarrow{}  T.  \mforall{}e:E.
                (P[base]
                {}\mRightarrow{}  (\mforall{}x:T.  \mforall{}e':E(X).    ((e'  <loc  e)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  P[f  x  X(e')]))
                {}\mRightarrow{}  P[prior-state(f;base;X;e)])


By

---

Latex:
((LocLessInd  THEN  Auto)  THEN  RecUnfold  `es-local-prior-state`  0  THEN  SplitOnConclITE  THEN  Auto)

---

Home Index