---

Step * 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. L : Base
7. L1 : Base
8. L = L1 ∈ (T List)
⊢ ∀n:ℕ. ∀L,L2:Base.  ((L = L2 ∈ (T List)) ⇒ (colength(L) = n ∈ ℤ) ⇒ (F[L] = F[L2] ∈ A))
BY
{ (RepeatFor 3 (Thin (-1))
   THEN InductionOnNat
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (D 0 THENA (GenConcl ⌜L2 = X ∈ (T List)⌝⋅ THEN Auto))
   THEN (ApFunToHypEquands `Z' ⌜colength(Z)⌝ ⌜ℕ⌝ (-2)⋅ THENA Auto)) }

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. L : Base
8. L2 : Base
9. L = L2 ∈ (T List)
10. colength(L) = 0 ∈ ℤ
11. colength(L) = colength(L2) ∈ ℕ
⊢ F[L] = F[L2] ∈ A

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) ∈ ℕ
⊢ F[L] = F[L2] ∈ A

---

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.  L  :  Base
7.  L1  :  Base
8.  L  =  L1
\mvdash{}  \mforall{}n:\mBbbN{}.  \mforall{}L,L2:Base.    ((L  =  L2)  {}\mRightarrow{}  (colength(L)  =  n)  {}\mRightarrow{}  (F[L]  =  F[L2]))


By

---

Latex:
(RepeatFor  3  (Thin  (-1))
  THEN  InductionOnNat
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (D  0  THENA  (GenConcl  \mkleeneopen{}L2  =  X\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (ApFunToHypEquands  `Z'  \mkleeneopen{}colength(Z)\mkleeneclose{}  \mkleeneopen{}\mBbbN{}\mkleeneclose{}  (-2)\mcdot{}  THENA  Auto))

---

Home Index