Proof of Nuprl Lemma : es-last-event

Step * 1 2 1 1 of Lemma es-last-event_wf

1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| e' ≤loc e1 }  ─→ 𝔹
           (es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
                                              ∧ (↑(P e'))

                                              ∧ (∀e'':E. ((e' <loc e'')

⇒ e'' ≤loc e1  ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| (e' ≤loc e1  ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e }  ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
                                          ∧ (↑(P e'))
                                          ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})))
13. x : ∃e':{E| (e' ≤loc pred(e)
                ∧ (↑(P e'))
                ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))} + (¬(∃e':{E| (e' ≤loc pred(e)

                                                                                               ∧ (↑(P e')))}))@i

⊢ x ∈ ∃e':{E| (e' ≤loc e ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e ⇒ (¬↑(P e'')))))} + (¬(∃e':{E

                                                                                                    (e' ≤loc e

                                                                                                    ∧ (↑(P e')))}))

BY
{ (D (-1) THEN MemCD) }

1
.....subterm..... T:t
1:n
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| e' ≤loc e1 }  ─→ 𝔹
           (es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
                                              ∧ (↑(P e'))

                                              ∧ (∀e'':E. ((e' <loc e'')

⇒ e'' ≤loc e1  ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| (e' ≤loc e1  ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e }  ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
                                          ∧ (↑(P e'))
                                          ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})))
13. x1 : ∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))}@i
⊢ x1 ∈ ∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬↑(P e'')))))}

2
.....eq aux.....
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| e' ≤loc e1 }  ─→ 𝔹
           (es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
                                              ∧ (↑(P e'))

                                              ∧ (∀e'':E. ((e' <loc e'')

⇒ e'' ≤loc e1  ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| (e' ≤loc e1  ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e }  ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
                                          ∧ (↑(P e'))
                                          ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})))
13. x1 : ∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))}@i
⊢ ¬(∃e':{E| (e' ≤loc e  ∧ (↑(P e')))}) ∈ Type

3
.....subterm..... T:t
1:n
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| e' ≤loc e1 }  ─→ 𝔹
           (es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
                                              ∧ (↑(P e'))

                                              ∧ (∀e'':E. ((e' <loc e'')

⇒ e'' ≤loc e1  ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| (e' ≤loc e1  ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e }  ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
                                          ∧ (↑(P e'))
                                          ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})))
13. y : ¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})@i
⊢ y ∈ ¬(∃e':{E| (e' ≤loc e  ∧ (↑(P e')))})

4
.....eq aux.....
1. es : EO
2. e : E@i
3. ¬↑first(e)
4. ∀e1:E
     ((e1 < e)
     ⇒ (∀P:{e':E| e' ≤loc e1 }  ─→ 𝔹
           (es-last-event(es;P;e1) ∈ (∃e':{E| (e' ≤loc e1
                                              ∧ (↑(P e'))

                                              ∧ (∀e'':E. ((e' <loc e'')

⇒ e'' ≤loc e1  ⇒ (¬↑(P e'')))))})
            ∨ (¬(∃e':{E| (e' ≤loc e1  ∧ (↑(P e')))})))))
5. P : {e':E| e' ≤loc e }  ─→ 𝔹@i
6. ¬↑(P e)
7. es-last-event(es;P;pred(e)) ∈ (∃e':{E| (e' ≤loc pred(e)
                                          ∧ (↑(P e'))
                                          ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
   ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))}))
8. loc(pred(e)) = loc(e) ∈ Id
9. (pred(e) < e)
10. ∀e':E. (e' < e) ⇒ ((e' = pred(e) ∈ E) ∨ (e' < pred(e))) supposing loc(e') = loc(e) ∈ Id
11. (pred(e) <loc e)
12. es-last-event(es;P;pred(e))
= es-last-event(es;P;pred(e))
∈ ((∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc pred(e)  ⇒ (¬↑(P e'')))))})
  ∨ (¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})))
13. y : ¬(∃e':{E| (e' ≤loc pred(e)  ∧ (↑(P e')))})@i
⊢ ∃e':{E| (e' ≤loc e  ∧ (↑(P e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬↑(P e'')))))} ∈ Type

Latex:

1. es : EO 2. e : E@i 3. \mneg{}\muparrow{}first(e) 4. \mforall{}e1:E ((e1 < e) {}\mRightarrow{} (\mforall{}P:\{e':E| e' \mleq{}loc e1 \} {}\mrightarrow{} \mBbbB{} (es-last-event(es;P;e1) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc e1 \mwedge{} (\muparrow{}(P e')) \mwedge{} (\mforall{}e'':E ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc e1 {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\}) \mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc e1 \mwedge{} (\muparrow{}(P e')))\}))))) 5. P : \{e':E| e' \mleq{}loc e \} {}\mrightarrow{} \mBbbB{}@i 6. \mneg{}\muparrow{}(P e) 7. es-last-event(es;P;pred(e)) \mmember{} (\mexists{}e':\{E| (e' \mleq{}loc pred(e) \mwedge{} (\muparrow{}(P e')) \mwedge{} (\mforall{}e'':E ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc pred(e) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\}) \mvee{} (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc pred(e) \mwedge{} (\muparrow{}(P e')))\})) 8. loc(pred(e)) = loc(e) 9. (pred(e) < e) 10. \mforall{}e':E. (e' < e) {}\mRightarrow{} ((e' = pred(e)) \mvee{} (e' < pred(e))) supposing loc(e') = loc(e) 11. (pred(e) <loc e) 12. es-last-event(es;P;pred(e)) = es-last-event(es;P;pred(e)) 13. x : \mexists{}e':\{E| (e' \mleq{}loc pred(e) \mwedge{} (\muparrow{}(P e')) \mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc pred(e) {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\} + (\mneg{}(\mexists{}e':\{E (e' \mleq{}loc pred(e) \mwedge{} (\muparrow{}(P e')))\}))@i \mvdash{} x \mmember{} \mexists{}e':\{E| (e' \mleq{}loc e \mwedge{} (\muparrow{}(P e')) \mwedge{} (\mforall{}e'':E. ((e' <loc e'') {}\mRightarrow{} e'' \mleq{}loc e {}\mRightarrow{} (\mneg{}\muparrow{}(P e'')))))\} + (\mneg{}(\mexists{}e':\{E| (e' \mleq{}loc e \mwedge{} (\muparrow{}(P e')))\})) By (D (-1) THEN MemCD) Home Index