---

Step * 1 1 1 1 of Lemma lifting-gen-list-rev_wf


1. B : Type
2. n : ℕ
3. p : ℤ
4. 0 < p
5. 0 ≤ n - p - 1 < n + 1
⇒ (∀[A:ℕn ⟶ Type]. ∀[bags:k:ℕn ⟶ bag(A k)]. ∀[g:funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)].
      (lifting-gen-list-rev(n;bags) (n - p - 1) g ∈ bag(B)))
6. 0 ≤ (n - p)
7. n - p < n + 1
8. A : ℕn ⟶ Type
9. bags : k:ℕn ⟶ bag(A k)
10. g : funtype(p;λx.(A (x + (n - p)));B)
11. ¬(n = (n - p) ∈ ℤ)
12. x : A (n - p)
13. True
14. (n - n - p) = p ∈ ℤ
15. (n - (n - p) + 1) = (p - 1) ∈ ℤ
⊢ g x ∈ funtype(n - n - p - 1;λx.(A (x + (n - p - 1)));B)
BY
{ ((Unfold `funtype` (-6) THEN (RWO "primrec-unroll" (-6) THENA Auto) THEN Reduce (-6))
   THEN (Subst' (p - 1 - p - 1) + (n - p) ~ n - p -6 THENA Auto)
   THEN SplitOnHypITE -6 
   THEN Auto') }

---

Latex:

---

Latex:

1.  B  :  Type
2.  n  :  \mBbbN{}
3.  p  :  \mBbbZ{}
4.  0  <  p
5.  0  \mleq{}  n  -  p  -  1  <  n  +  1
{}\mRightarrow{}  (\mforall{}[A:\mBbbN{}n  {}\mrightarrow{}  Type].  \mforall{}[bags:k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)].
        \mforall{}[g:funtype(n  -  n  -  p  -  1;\mlambda{}x.(A  (x  +  (n  -  p  -  1)));B)].
            (lifting-gen-list-rev(n;bags)  (n  -  p  -  1)  g  \mmember{}  bag(B)))
6.  0  \mleq{}  (n  -  p)
7.  n  -  p  <  n  +  1
8.  A  :  \mBbbN{}n  {}\mrightarrow{}  Type
9.  bags  :  k:\mBbbN{}n  {}\mrightarrow{}  bag(A  k)
10.  g  :  funtype(p;\mlambda{}x.(A  (x  +  (n  -  p)));B)
11.  \mneg{}(n  =  (n  -  p))
12.  x  :  A  (n  -  p)
13.  True
14.  (n  -  n  -  p)  =  p
15.  (n  -  (n  -  p)  +  1)  =  (p  -  1)
\mvdash{}  g  x  \mmember{}  funtype(n  -  n  -  p  -  1;\mlambda{}x.(A  (x  +  (n  -  p  -  1)));B)


By

---

Latex:
((Unfold  `funtype`  (-6)  THEN  (RWO  "primrec-unroll"  (-6)  THENA  Auto)  THEN  Reduce  (-6))
  THEN  (Subst'  (p  -  1  -  p  -  1)  +  (n  -  p)  \msim{}  n  -  p  -6  THENA  Auto)
  THEN  SplitOnHypITE  -6 
  THEN  Auto')

---

Home Index