Proof of Nuprl Lemma : es-rec-class

Step * 1 1 1 of Lemma es-rec-class_wf

1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)}  ─→ bag(T)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e1 ∈ bag(T)))
8. x : E@i
9. (x <loc e)@i
10. ↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x) =_z 1)@i
11. ∀e'':E
      ((x <loc e'')
      ⇒ (e'' <loc e)
      ⇒

 (¬↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e'') =_z 1)))@i

12. (last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e)

= (inl x)
∈ ((∃e':{E| ((e' <loc e)

            ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e'))

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

 (¬↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)

               ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

e')))})))@i

⊢ F[es;x;only(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x);e] ∈ bag(T)

{ (Assert #(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x) = 1 ∈ ℤ BY

         (RW assert_pushdownC (-3) THEN Auto)) }

1
.....wf.....
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)}  ─→ bag(T)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e1 ∈ bag(T)))
8. x : E@i
9. (x <loc e)@i
10. ↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x) =_z 1)@i
11. ∀e'':E
      ((x <loc e'')
      ⇒ (e'' <loc e)
      ⇒

 (¬↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e'') =_z 1)))@i

12. (last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e)

= (inl x)
∈ ((∃e':{E| ((e' <loc e)

            ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e'))

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

 (¬↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)

               ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

                    e')))})))@i
⊢ #(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x) ∈ ℤ

2
1. Info : Type
2. T : Type
3. G : es:EO+(Info) ─→ E ─→ bag(T)
4. F : es:EO+(Info) ─→ e':E ─→ T ─→ {e:E| (e' <loc e)}  ─→ bag(T)
5. es : EO+(Info)
6. e : E@i
7. ∀e1:E. ((e1 < e) ⇒ (RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e1 ∈ bag(T)))
8. x : E@i
9. (x <loc e)@i
10. ↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x) =_z 1)@i
11. ∀e'':E
      ((x <loc e'')
      ⇒ (e'' <loc e)
      ⇒

 (¬↑(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e'') =_z 1)))@i

12. (last(λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e)

= (inl x)
∈ ((∃e':{E| ((e' <loc e)

            ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1)) e'))

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

 (¬↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

e'')))))})
∨ (¬(∃e':{E| ((e' <loc e)

               ∧ (↑((λe.(#(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es e) =_z 1))

e')))})))@i
13. #(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es x) = 1 ∈ ℤ

⊢ F[es;x;only(RecClass(first e  G[es;e]or next e after e' with value v    F[es;e';v;e]) es x);e] ∈ bag(T)

Latex:

Latex:
1. Info : Type 2. T : Type 3. G : es:EO+(Info) {}\mrightarrow{} E {}\mrightarrow{} bag(T) 4. F : es:EO+(Info) {}\mrightarrow{} e':E {}\mrightarrow{} T {}\mrightarrow{} \{e:E| (e' <loc e)\} {}\mrightarrow{} bag(T) 5. es : EO+(Info) 6. e : E@i 7. \mforall{}e1:E ((e1 < e) {}\mRightarrow{} (RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es e1 \mmember{} bag(T))) 8. x : E@i 9. (x <loc e)@i 10. \muparrow{}(\#(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es x) =\msubz{} 1)@i 11. \mforall{}e'':E ((x <loc e'') {}\mRightarrow{} (e'' <loc e) {}\mRightarrow{} (\mneg{}\muparrow{}(\#(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es e'') =\msubz{} 1)))@i 12. (last(\mlambda{}e.(\#(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es e) =\msubz{} 1)) e) = (inl x)@i \mvdash{} F[es;x;only(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es x);e] \mmember{} bag(T) By Latex: (Assert \#(RecClass(first e G[es;e]or next e after e' with value v F[es;e';v;e]) es x) = 1 BY (RW assert\_pushdownC (-3) THEN Auto)) Home Index