Step
*
1
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)))
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)
BY
{ ((InstHyp [⌜t⌝] (-4)⋅ THENA Auto)
THEN (Subst' (n + n1) + 1 ~ n + n1 + 1 0 THENA Auto)
THEN NthHypSq (-1)
THEN RepeatFor 2 (EqCD)
THEN Try (Trivial)) }
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
16. 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))
⊢ seq-append(n + n1;1;seq-append(n;n1;s;s1);λi.t) ~ seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m))
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. 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
16. 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))
⊢ λm.if m=n + n1 then t else (seq-append(n;n1;s;s1) m) ~ seq-append(n;n1 + 1;s;λm.if m=n1 then t else (s1 m))
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)))
13. y : \mneg{}(R (n + n1) seq-append(n;n1;s;s1))
14. (d (n + n1) seq-append(n;n1;s;s1)) = (inr y )
15. t : T
\mvdash{} 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) + 1) seq-append(n + n1;1;seq-append(n;n1;s;s1);\mlambda{}i.t)
By
Latex:
((InstHyp [\mkleeneopen{}t\mkleeneclose{}] (-4)\mcdot{} THENA Auto)
THEN (Subst' (n + n1) + 1 \msim{} n + n1 + 1 0 THENA Auto)
THEN NthHypSq (-1)
THEN RepeatFor 2 (EqCD)
THEN Try (Trivial))
Home
Index