---

Step * 1 1 2 1 1 1 of Lemma list-functionality-induction

.....assertion..... 
1. T : Type
2. A : Type
3. F : Base
4. F[[]] ∈ A
5. ∀a1,a2,L1,L2:Base.  ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A))
6. n : ℤ
7. 0 < n
8. ∀L,L2:Base.  ((L = L2 ∈ (T List)) ⇒ (colength(L) = (n - 1) ∈ ℤ) ⇒ (F[L] = F[L2] ∈ A))
9. L : Base
10. L2 : Base
11. L = L2 ∈ (T List)
12. colength(L) = n ∈ ℤ
13. colength(L) = colength(L2) ∈ ℕ
14. fst(L) ∈ T
15. snd(L) ∈ T List
16. colength(L) = (1 + colength(snd(L))) ∈ ℤ
17. L ~ [fst(L) / (snd(L))]
18. fst(L2) ∈ T
19. snd(L2) ∈ T List
20. colength(L2) = (1 + colength(snd(L2))) ∈ ℤ
21. L2 ~ [fst(L2) / (snd(L2))]
⊢ L = L2 ∈ (T × (T List))
BY
{ SubsumeC ⌜{X:T List| 0 < colength(X)} ⌝⋅ }

1
1. T : Type
2. A : Type
3. F : Base
4. F[[]] ∈ A
5. ∀a1,a2,L1,L2:Base.  ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A))
6. n : ℤ
7. 0 < n
8. ∀L,L2:Base.  ((L = L2 ∈ (T List)) ⇒ (colength(L) = (n - 1) ∈ ℤ) ⇒ (F[L] = F[L2] ∈ A))
9. L : Base
10. L2 : Base
11. L = L2 ∈ (T List)
12. colength(L) = n ∈ ℤ
13. colength(L) = colength(L2) ∈ ℕ
14. fst(L) ∈ T
15. snd(L) ∈ T List
16. colength(L) = (1 + colength(snd(L))) ∈ ℤ
17. L ~ [fst(L) / (snd(L))]
18. fst(L2) ∈ T
19. snd(L2) ∈ T List
20. colength(L2) = (1 + colength(snd(L2))) ∈ ℤ
21. L2 ~ [fst(L2) / (snd(L2))]
⊢ L = L2 ∈ {X:T List| 0 < colength(X)} 

2
1. T : Type
2. A : Type
3. F : Base
4. F[[]] ∈ A
5. ∀a1,a2,L1,L2:Base.  ((a1 = a2 ∈ T) ⇒ (F[L1] = F[L2] ∈ A) ⇒ (F[[a1 / L1]] = F[[a2 / L2]] ∈ A))
6. n : ℤ
7. 0 < n
8. ∀L,L2:Base.  ((L = L2 ∈ (T List)) ⇒ (colength(L) = (n - 1) ∈ ℤ) ⇒ (F[L] = F[L2] ∈ A))
9. L : Base
10. L2 : Base
11. L = L2 ∈ (T List)
12. colength(L) = n ∈ ℤ
13. colength(L) = colength(L2) ∈ ℕ
14. fst(L) ∈ T
15. snd(L) ∈ T List
16. colength(L) = (1 + colength(snd(L))) ∈ ℤ
17. L ~ [fst(L) / (snd(L))]
18. fst(L2) ∈ T
19. snd(L2) ∈ T List
20. colength(L2) = (1 + colength(snd(L2))) ∈ ℤ
21. L2 ~ [fst(L2) / (snd(L2))]
22. L = L2 ∈ {X:T List| 0 < colength(X)} 
⊢ {X:T List| 0 < colength(X)}  ⊆r (T × (T List))

---

Latex:

---

Latex:
.....assertion..... 
1.  T  :  Type
2.  A  :  Type
3.  F  :  Base
4.  F[[]]  \mmember{}  A
5.  \mforall{}a1,a2,L1,L2:Base.    ((a1  =  a2)  {}\mRightarrow{}  (F[L1]  =  F[L2])  {}\mRightarrow{}  (F[[a1  /  L1]]  =  F[[a2  /  L2]]))
6.  n  :  \mBbbZ{}
7.  0  <  n
8.  \mforall{}L,L2:Base.    ((L  =  L2)  {}\mRightarrow{}  (colength(L)  =  (n  -  1))  {}\mRightarrow{}  (F[L]  =  F[L2]))
9.  L  :  Base
10.  L2  :  Base
11.  L  =  L2
12.  colength(L)  =  n
13.  colength(L)  =  colength(L2)
14.  fst(L)  \mmember{}  T
15.  snd(L)  \mmember{}  T  List
16.  colength(L)  =  (1  +  colength(snd(L)))
17.  L  \msim{}  [fst(L)  /  (snd(L))]
18.  fst(L2)  \mmember{}  T
19.  snd(L2)  \mmember{}  T  List
20.  colength(L2)  =  (1  +  colength(snd(L2)))
21.  L2  \msim{}  [fst(L2)  /  (snd(L2))]
\mvdash{}  L  =  L2


By

---

Latex:
SubsumeC  \mkleeneopen{}\{X:T  List|  0  <  colength(X)\}  \mkleeneclose{}\mcdot{}

---

Home Index