Step
*
1
2
1
2
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
⊢ ↓∃lst:k:{n - p..n-} ⟶ (A k). ((∀[k:{n - p..n-}]. lst k ↓∈ bags k) ∧ ((uncurry-gen(n) (n - p) (λx.f) lst) = b ∈ B))
BY
{ (D 0 THEN (InstConcl [⌜λr.if (r =z n - p) then x else lst r fi ⌝]⋅ THENA Auto)) }
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)
∧ ((uncurry-gen(n) (n - p) (λx.f) (λr.if (r =z n - p) then x else lst r fi )) = b ∈ B)
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)
9. n - p < n + 1
10. f : (A (n - p)) ⟶ primrec(p - 1;B;λi,t. ((A ((p - 1 - i) + (n - p))) ⟶ t))
11. ∀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))))
12. x : A (n - p)
13. x ↓∈ bags (n - p)
14. b ↓∈ lifting-gen-list-rev(n;bags) ((n - p) + 1) (f x)
15. lst : k:{(n - p) + 1..n-} ⟶ (A k)
16. ∀[k:{(n - p) + 1..n-}]. lst k ↓∈ bags k
17. (uncurry-gen(n) ((n - p) + 1) (λx@0.(f x)) lst) = b ∈ B
18. l1 : k:{n - p..n-} ⟶ (A k)
19. x1 : ∀[k:{n - p..n-}]. l1 k ↓∈ bags k
⊢ uncurry-gen(n) (n - p) (λx.f) l1 ∈ 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{} \mdownarrow{}\mexists{}lst:k:\{n - p..n\msupminus{}\} {}\mrightarrow{} (A k)
((\mforall{}[k:\{n - p..n\msupminus{}\}]. lst k \mdownarrow{}\mmember{} bags k) \mwedge{} ((uncurry-gen(n) (n - p) (\mlambda{}x.f) lst) = b))
By
Latex:
(D 0 THEN (InstConcl [\mkleeneopen{}\mlambda{}r.if (r =\msubz{} n - p) then x else lst r fi \mkleeneclose{}]\mcdot{} THENA Auto))
Home
Index