Step
*
1
2
1
2
1
1
1
of Lemma
lifting-member
1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. bags : k:ℕn ⟶ bag(A k)
5. b : B
6. p : ℤ
7. 0 < p
8. 0 ≤ n - p < n + 1
9. f : (A (n - p)) ⟶ primrec(p - 1;B;λi,t. ((A ((p - 1 - i) + (n - p))) ⟶ t))
10. ∀f:funtype(p - 1;λx.(A (x + (n - p) + 1));B)
(b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) f
⇒ (↓∃lst:k:{(n - p) + 1..n-} ⟶ (A k)
((∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) ((n - p) + 1) (λx.f) lst) = b ∈ B))))
11. x : A (n - p)
12. x ↓∈ bags (n - p)
13. b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) (f x)
14. lst : k:{(n - p) + 1..n-} ⟶ (A k)
15. ∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k
16. (uncurry-gen(n) ((n - p) + 1) (λx@0.(f x)) lst) = b ∈ B
⊢ (∀[k:{n - p..n-}]. (λr.if (r =z n - p) then x else lst r fi ) k ↓∈ bags k)
∧ ((uncurry-gen(n) (n - p) (λx.f) (λr.if (r =z n - p) then x else lst r fi )) = b ∈ B)
BY
{ D 0 }
1
1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. bags : k:ℕn ⟶ bag(A k)
5. b : B
6. p : ℤ
7. 0 < p
8. 0 ≤ n - p < n + 1
9. f : (A (n - p)) ⟶ primrec(p - 1;B;λi,t. ((A ((p - 1 - i) + (n - p))) ⟶ t))
10. ∀f:funtype(p - 1;λx.(A (x + (n - p) + 1));B)
(b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) f
⇒ (↓∃lst:k:{(n - p) + 1..n-} ⟶ (A k)
((∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) ((n - p) + 1) (λx.f) lst) = b ∈ B))))
11. x : A (n - p)
12. x ↓∈ bags (n - p)
13. b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) (f x)
14. lst : k:{(n - p) + 1..n-} ⟶ (A k)
15. ∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k
16. (uncurry-gen(n) ((n - p) + 1) (λx@0.(f x)) lst) = b ∈ B
⊢ ∀[k:{n - p..n-}]. (λr.if (r =z n - p) then x else lst r fi ) k ↓∈ bags k
2
1. B : Type
2. n : ℕ
3. A : ℕn ⟶ Type
4. bags : k:ℕn ⟶ bag(A k)
5. b : B
6. p : ℤ
7. 0 < p
8. 0 ≤ n - p < n + 1
9. f : (A (n - p)) ⟶ primrec(p - 1;B;λi,t. ((A ((p - 1 - i) + (n - p))) ⟶ t))
10. ∀f:funtype(p - 1;λx.(A (x + (n - p) + 1));B)
(b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) f
⇒ (↓∃lst:k:{(n - p) + 1..n-} ⟶ (A k)
((∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) ((n - p) + 1) (λx.f) lst) = b ∈ B))))
11. x : A (n - p)
12. x ↓∈ bags (n - p)
13. b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) (f x)
14. lst : k:{(n - p) + 1..n-} ⟶ (A k)
15. ∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k
16. (uncurry-gen(n) ((n - p) + 1) (λx@0.(f x)) lst) = b ∈ B
⊢ (uncurry-gen(n) (n - p) (λx.f) (λr.if (r =z n - p) then x else lst r fi )) = b ∈ B
Latex:
Latex:
1. B : Type
2. n : \mBbbN{}
3. A : \mBbbN{}n {}\mrightarrow{} Type
4. bags : k:\mBbbN{}n {}\mrightarrow{} bag(A k)
5. b : B
6. p : \mBbbZ{}
7. 0 < p
8. 0 \mleq{} n - p < n + 1
9. f : (A (n - p)) {}\mrightarrow{} primrec(p - 1;B;\mlambda{}i,t. ((A ((p - 1 - i) + (n - p))) {}\mrightarrow{} t))
10. \mforall{}f:funtype(p - 1;\mlambda{}x.(A (x + (n - p) + 1));B)
(b \mdownarrow{}\mmember{} lifting-gen-list-rev(n;bags) ((n - p) + 1) f
{}\mRightarrow{} (\mdownarrow{}\mexists{}lst:k:\{(n - p) + 1..n\msupminus{}\} {}\mrightarrow{} (A k)
((\mforall{}[k:\{(n - p) + 1..n\msupminus{}\}]. lst k \mdownarrow{}\mmember{} bags k)
\mwedge{} ((uncurry-gen(n) ((n - p) + 1) (\mlambda{}x.f) lst) = b))))
11. x : A (n - p)
12. x \mdownarrow{}\mmember{} bags (n - p)
13. b \mdownarrow{}\mmember{} lifting-gen-list-rev(n;bags) ((n - p) + 1) (f x)
14. lst : k:\{(n - p) + 1..n\msupminus{}\} {}\mrightarrow{} (A k)
15. \mforall{}[k:\{(n - p) + 1..n\msupminus{}\}]. lst k \mdownarrow{}\mmember{} bags k
16. (uncurry-gen(n) ((n - p) + 1) (\mlambda{}x@0.(f x)) lst) = b
\mvdash{} (\mforall{}[k:\{n - p..n\msupminus{}\}]. (\mlambda{}r.if (r =\msubz{} n - p) then x else lst r fi ) k \mdownarrow{}\mmember{} bags k)
\mwedge{} ((uncurry-gen(n) (n - p) (\mlambda{}x.f) (\mlambda{}r.if (r =\msubz{} n - p) then x else lst r fi )) = b)
By
Latex:
D 0
Home
Index