Proof of Nuprl Lemma : bar_recursion

Step * 1 1 of Lemma bar_recursion_wf

1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. d : ∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R n s)
5. b : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((R n s) ⇒ (A n s))
6. i : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. (A (n + 1) seq-append(n;1;s;λi.t))) ⇒ (A n s))
7. n : ℕ
8. s : ℕn ⟶ T
9. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R (n + m) seq-append(n;m;s;alpha)))
10. n1 : ℕ
11. s1 : ℕn1 ⟶ T
12. ∀t:T
      (bar_recursion(d;
                     b;
                     i;

                     n + n1 + 1;seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m))) ∈ A (n + n1 + 1)

                                                                          seq-append(n;n1 + 1;s;λm.if m=n1

                                                                                                   then t

                                                                                                   else (s1 m)))

⊢ case d (n + n1) seq-append(n;n1;s;s1)
   of inl(r) =>
   b (n + n1) seq-append(n;n1;s;s1) r
   | inr(r) =>
   i (n + n1) seq-append(n;n1;s;s1)
   (λt.bar_recursion(d;
                     b;
                     i;

                     (n + n1) + 1;λm.if m=n + n1 then t else (seq-append(n;n1;s;s1) m))) ∈ A (n + n1) seq-append(n;n1;s;\000Cs1)

{ ((GenConclTerm ⌜d (n + n1) seq-append(n;n1;s;s1)⌝⋅ THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. R : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
3. A : n:ℕ ⟶ (ℕn ⟶ T) ⟶ ℙ
4. d : ∀n:ℕ. ∀s:ℕn ⟶ T.  Dec(R n s)
5. b : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((R n s) ⇒ (A n s))
6. i : ∀n:ℕ. ∀s:ℕn ⟶ T.  ((∀t:T. (A (n + 1) seq-append(n;1;s;λi.t))) ⇒ (A n s))
7. n : ℕ
8. s : ℕn ⟶ T
9. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R (n + m) seq-append(n;m;s;alpha)))
10. n1 : ℕ
11. s1 : ℕn1 ⟶ T
12. ∀t:T
      (bar_recursion(d;
                     b;
                     i;

                     n + n1 + 1;seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m))) ∈ A (n + n1 + 1)

                                                                          seq-append(n;n1 + 1;s;λm.if m=n1

                                                                                                   then t

                                                                                                   else (s1 m)))

13. y : ¬(R (n + n1) seq-append(n;n1;s;s1))
14. (d (n + n1) seq-append(n;n1;s;s1)) = (inr y ) ∈ Dec(R (n + n1) seq-append(n;n1;s;s1))
15. t : T
⊢ bar_recursion(d;
b;
i;

                (n + n1) + 1;λm.if m=n + n1 then t else (seq-append(n;n1;s;s1) m)) ∈ A ((n + n1) + 1)

                                                                       seq-append(n + n1;1;seq-append(n;n1;s;s1);λi.t)

Latex:

Latex:
1. T : Type 2. R : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbP{} 3. A : n:\mBbbN{} {}\mrightarrow{} (\mBbbN{}n {}\mrightarrow{} T) {}\mrightarrow{} \mBbbP{} 4. d : \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} T. Dec(R n s) 5. b : \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} T. ((R n s) {}\mRightarrow{} (A n s)) 6. i : \mforall{}n:\mBbbN{}. \mforall{}s:\mBbbN{}n {}\mrightarrow{} T. ((\mforall{}t:T. (A (n + 1) seq-append(n;1;s;\mlambda{}i.t))) {}\mRightarrow{} (A n s)) 7. n : \mBbbN{} 8. s : \mBbbN{}n {}\mrightarrow{} T 9. \mforall{}alpha:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}m:\mBbbN{}. (R (n + m) seq-append(n;m;s;alpha))) 10. n1 : \mBbbN{} 11. s1 : \mBbbN{}n1 {}\mrightarrow{} T 12. \mforall{}t:T (bar\_recursion(d; b; i; n + n1 + 1;seq-append(n;n1 + 1;s;\mlambda{}m.if m=n1 then t else (s1 m))) \mmember{} A (n + n1 + \000C1) seq-append(n;n1 + 1;s;\mlambda{}m.if m=n1 then t else (s1 m))) \mvdash{} case d (n + n1) seq-append(n;n1;s;s1) of inl(r) => b (n + n1) seq-append(n;n1;s;s1) r | inr(r) => i (n + n1) seq-append(n;n1;s;s1) (\mlambda{}t.bar\_recursion(d; b; i; (n + n1) + 1;\mlambda{}m.if m=n + n1 then t else (seq-append(n;n1;s;s1) m))) \mmember{} A (n + n1\000C) seq-append(n;n1;s;s1) By Latex: ((GenConclTerm \mkleeneopen{}d (n + n1) seq-append(n;n1;s;s1)\mkleeneclose{}\mcdot{} THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto) Home Index