Proof of Nuprl Lemma : State-comb-fun-eq

Step * 2 1 of Lemma State-comb-fun-eq

1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬((X es e) = {} ∈ bag(A))
10. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈_b X
⊢ sv-bag-only(lifting-2(f) (X es e)

              (Prior(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init))?init es e))

= (f sv-bag-only(X es e)

   sv-bag-only(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es pred(e)))

∈ B
BY
{ (RepUR ``primed-class-opt`` 0 THEN GenConclAtAddr [2;1;2;1]) }

1
.....wf.....
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬((X es e) = {} ∈ bag(A))
10. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈_b X

⊢ last(λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e')) e ∈ (∃e\000C':{E

((e' <loc e)

  ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e')) e'))

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

 (¬↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e'))\000C

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

               ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) e\000Cs

e'))
e')))}))

2
.....wf.....
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬((X es e) = {} ∈ bag(A))
10. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈_b X
⊢ (∃e':{E| ((e' <loc e)

           ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e'\000C))

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

 (¬↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init\000C) es

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

               ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) e\000Cs

e'))
e')))})) ∈ ℙ

3
1. Info : Type
2. B : Type
3. A : Type
4. f : A ─→ B ─→ B
5. init : Id ─→ bag(B)
6. X : EClass(A)
7. es : EO+(Info)
8. e : E
9. ¬((X es e) = {} ∈ bag(A))
10. ¬↑first(e)
11. ∀l:Id. (1 ≤ #(init l))
12. ∀l:Id. single-valued-bag(init l;B)
13. single-valued-classrel(es;X;A)
14. ↑e ∈_b X
15. v : (∃e':{E| ((e' <loc e)

                 ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init)\000C es

                                  e'))
                      e'))
                 ∧ (∀e'':E
                      ((e' <loc e'')
                      ⇒ (e'' <loc e)
                      ⇒ (¬↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0)

                                                                   then s

                                                                   else lifting-2(f) (w 0) s

                                                                   fi ;init)

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

             ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es \000Ce'))

e')))}))@i

16. (last(λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e')) e)

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

            ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e\000C'))

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

 (¬↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;ini\000Ct) es

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

               ∧ (↑((λe'.0 <z #(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) e\000Cs

                                e'))
                    e')))})))@i
⊢ sv-bag-only(lifting-2(f) (X es e)
              case v
               of inl(e') =>

               rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es e'

| inr(x) =>
init loc(e))
= (f sv-bag-only(X es e)

   sv-bag-only(rec-comb(λn.[X][n];λi,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init) es pred(e)))

∈ B

Latex:

Latex:
1. Info : Type 2. B : Type 3. A : Type 4. f : A {}\mrightarrow{} B {}\mrightarrow{} B 5. init : Id {}\mrightarrow{} bag(B) 6. X : EClass(A) 7. es : EO+(Info) 8. e : E 9. \mneg{}((X es e) = \{\}) 10. \mneg{}\muparrow{}first(e) 11. \mforall{}l:Id. (1 \mleq{} \#(init l)) 12. \mforall{}l:Id. single-valued-bag(init l;B) 13. single-valued-classrel(es;X;A) 14. \muparrow{}e \mmember{}\msubb{} X \mvdash{} sv-bag-only(lifting-2(f) (X es e) (Prior(rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init))?init es e)) = (f sv-bag-only(X es e) sv-bag-only(rec-comb(\mlambda{}n.[X][n];\mlambda{}i,w,s. if bag-null(w 0) then s else lifting-2(f) (w 0) s fi ;init\000C) es pred(e))) By Latex: (RepUR ``primed-class-opt`` 0 THEN GenConclAtAddr [2;1;2;1]) Home Index