Step
*
1
1
2
2
2
1
of Lemma
bar_recursion_wf1
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. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R m alpha))
8. c : Top
9. n : ℕ
10. s : ℕn ⟶ T
11. ∀t:T. (bar_recursion(d;b;i;n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m)))
12. y : ¬(R n s)
13. (d n s) = (inr y ) ∈ Dec(R n s)
14. t : T
15. bar_recursion(d;
b;
i;
n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m))
⊢ bar_recursion(d;
b;
i;
n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) seq-append(n;1;s;λi.t)
BY
{ Assert ⌜(A (n + 1) (λm.if m=n then t else (s m))) = (A (n + 1) seq-append(n;1;s;λi.t)) ∈ ℙ⌝⋅ }
1
.....assertion.....
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. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R m alpha))
8. c : Top
9. n : ℕ
10. s : ℕn ⟶ T
11. ∀t:T. (bar_recursion(d;b;i;n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m)))
12. y : ¬(R n s)
13. (d n s) = (inr y ) ∈ Dec(R n s)
14. t : T
15. bar_recursion(d;
b;
i;
n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m))
⊢ (A (n + 1) (λm.if m=n then t else (s m))) = (A (n + 1) seq-append(n;1;s;λi.t)) ∈ ℙ
2
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. ∀alpha:ℕ ⟶ T. (↓∃m:ℕ. (R m alpha))
8. c : Top
9. n : ℕ
10. s : ℕn ⟶ T
11. ∀t:T. (bar_recursion(d;b;i;n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m)))
12. y : ¬(R n s)
13. (d n s) = (inr y ) ∈ Dec(R n s)
14. t : T
15. bar_recursion(d;
b;
i;
n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) (λm.if m=n then t else (s m))
16. (A (n + 1) (λm.if m=n then t else (s m))) = (A (n + 1) seq-append(n;1;s;λi.t)) ∈ ℙ
⊢ bar_recursion(d;
b;
i;
n + 1;λm.if m=n then t else (s m)) ∈ A (n + 1) seq-append(n;1;s;λ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. \mforall{}alpha:\mBbbN{} {}\mrightarrow{} T. (\mdownarrow{}\mexists{}m:\mBbbN{}. (R m alpha))
8. c : Top
9. n : \mBbbN{}
10. s : \mBbbN{}n {}\mrightarrow{} T
11. \mforall{}t:T. (bar\_recursion(d;b;i;n + 1;\mlambda{}m.if m=n then t else (s m)) \mmember{} A (n + 1) (\mlambda{}m.if m=n then t \000Celse (s m)))
12. y : \mneg{}(R n s)
13. (d n s) = (inr y )
14. t : T
15. bar\_recursion(d;
b;
i;
n + 1;\mlambda{}m.if m=n then t else (s m)) \mmember{} A (n + 1) (\mlambda{}m.if m=n then t else (s m))
\mvdash{} bar\_recursion(d;
b;
i;
n + 1;\mlambda{}m.if m=n then t else (s m)) \mmember{} A (n + 1) seq-append(n;1;s;\mlambda{}i.t)
By
Latex:
Assert \mkleeneopen{}(A (n + 1) (\mlambda{}m.if m=n then t else (s m))) = (A (n + 1) seq-append(n;1;s;\mlambda{}i.t))\mkleeneclose{}\mcdot{}
Home
Index