---

Step * 2 2 2 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 ≤ (n - 0)
8. n - 0 < n + 1
9. f : funtype(n - n - 0;λx.(A (x + (n - 0)));B)
10. lst : k:{n - 0..n-} ⟶ (A k)
11. x : ∀[k:{n - 0..n-}]. lst k ↓∈ bags k
⊢ uncurry-gen(n) (n - 0) (λx.f) lst ∈ B
BY
{ (InstLemma `uncurry-gen_wf2` [⌜B⌝; ⌜n⌝; ⌜n - 0⌝; ⌜n - 0⌝; ⌜A⌝; ⌜λx.f⌝]⋅ THEN Auto) }

---

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  \mleq{}  (n  -  0)
8.  n  -  0  <  n  +  1
9.  f  :  funtype(n  -  n  -  0;\mlambda{}x.(A  (x  +  (n  -  0)));B)
10.  lst  :  k:\{n  -  0..n\msupminus{}\}  {}\mrightarrow{}  (A  k)
11.  x  :  \mforall{}[k:\{n  -  0..n\msupminus{}\}].  lst  k  \mdownarrow{}\mmember{}  bags  k
\mvdash{}  uncurry-gen(n)  (n  -  0)  (\mlambda{}x.f)  lst  \mmember{}  B


By

---

Latex:
(InstLemma  `uncurry-gen\_wf2`  [\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}n\mkleeneclose{};  \mkleeneopen{}n  -  0\mkleeneclose{};  \mkleeneopen{}n  -  0\mkleeneclose{};  \mkleeneopen{}A\mkleeneclose{};  \mkleeneopen{}\mlambda{}x.f\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index