---

Step * of Lemma es-local-pred-cases

∀[Info:Type]
  ∀es:EO+(Info). ∀e:E. ∀P:{e':E| (e' <loc e)}  ⟶ 𝔹.
    (¬↑first(e))
    ∧ (((↑(P pred(e))) ∧ (do-apply(last(P);e) = pred(e) ∈ E))
      ∨ ((¬↑(P pred(e))) ∧ (↑can-apply(last(P);pred(e))) ∧ (do-apply(last(P);e) = do-apply(last(P);pred(e)) ∈ E))) 
    supposing ↑can-apply(last(P);e)
BY
{ (InstLemma `es-local-pred-cases-sq` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (D 0
   THENM ((D (-2) THENA Auto)
          THEN (Try ((D -1 THEN D 0 THEN Try (Trivial) THEN D -1 THEN ExRepD THEN HypSubst (-1) 0))
                THEN Try (((OrLeft THENM Complete (Auto)) THEN Auto)⋅)
                THEN Try (((OrRight THENA Auto) THEN RepeatFor 2 ((D 0 THEN Try (Trivial))) THEN Fold `member` 0)))⋅
          )
   )) }

1
.....wf..... 
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ⟶ 𝔹@i
5. (¬↑first(e))
   ∧ (((↑(P pred(e))) ∧ (do-apply(last(P);e) ~ pred(e)))
     ∨ ((¬↑(P pred(e))) ∧ (↑can-apply(last(P);pred(e))) ∧ (do-apply(last(P);e) ~ do-apply(last(P);pred(e))))) 
   supposing ↑can-apply(last(P);e)
6. ↑can-apply(last(P);e)
⊢ can-apply(last(P);e) ∈ 𝔹

2
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ⟶ 𝔹@i
5. ↑can-apply(last(P);e)
6. ¬↑first(e)
7. ¬↑(P pred(e))
8. ↑can-apply(last(P);pred(e))
9. do-apply(last(P);e) ~ do-apply(last(P);pred(e))
⊢ do-apply(last(P);pred(e)) ∈ E

3
.....wf..... 
1. Info : Type
2. es : EO+(Info)@i'
3. e : E@i
4. P : {e':E| (e' <loc e)}  ⟶ 𝔹@i
5. (¬↑first(e))
   ∧ (((↑(P pred(e))) ∧ (do-apply(last(P);e) ~ pred(e)))
     ∨ ((¬↑(P pred(e))) ∧ (↑can-apply(last(P);pred(e))) ∧ (do-apply(last(P);e) ~ do-apply(last(P);pred(e))))) 
   supposing ↑can-apply(last(P);e)
⊢ ↑can-apply(last(P);e) ∈ ℙ

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}P:\{e':E|  (e'  <loc  e)\}    {}\mrightarrow{}  \mBbbB{}.
        (\mneg{}\muparrow{}first(e))
        \mwedge{}  (((\muparrow{}(P  pred(e)))  \mwedge{}  (do-apply(last(P);e)  =  pred(e)))
            \mvee{}  ((\mneg{}\muparrow{}(P  pred(e)))
                \mwedge{}  (\muparrow{}can-apply(last(P);pred(e)))
                \mwedge{}  (do-apply(last(P);e)  =  do-apply(last(P);pred(e))))) 
        supposing  \muparrow{}can-apply(last(P);e)


By

---

Latex:
(InstLemma  `es-local-pred-cases-sq`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (D  0
  THENM  ((D  (-2)  THENA  Auto)
                THEN  (Try  ((D  -1  THEN  D  0  THEN  Try  (Trivial)  THEN  D  -1  THEN  ExRepD  THEN  HypSubst  (-1)  0))
                            THEN  Try  (((OrLeft  THENM  Complete  (Auto))  THEN  Auto)\mcdot{})
                            THEN  Try  (((OrRight  THENA  Auto)
                                                  THEN  RepeatFor  2  ((D  0  THEN  Try  (Trivial)))
                                                  THEN  Fold  `member`  0)))\mcdot{}
                )
  ))

---

Home Index