---

Step * 1 1 1 1 1 of Lemma cons_functionality_wrt_permr


1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. ||as|| = ||bs|| ∈ ℤ
8. p : Sym(||as||)
9. ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)
10. (||as|| + 1) = (||bs|| + 1) ∈ ℤ
11. i : ℕ||as|| + 1
⊢ [a / as][(||as|| + 1) - 1 - if ((||as|| + 1) - 1 - i =z ||as||)
then (||as|| + 1) - 1 - i
else ||as|| - 1 - p.f (||as|| - 1 - (||as|| + 1) - 1 - i)
fi ]
= [b / bs][i]
∈ T
BY
{ (((SplitOnConclITE THENA Auto) THEN OnMCls [0; -1] (RW IntNormC)) THENA Auto) }

1
1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. ||as|| = ||bs|| ∈ ℤ
8. p : Sym(||as||)
9. ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)
10. (||as|| + 1) = (||bs|| + 1) ∈ ℤ
11. i : ℕ||as|| + 1
12. (((-1) * i) + ||as||) = ||as|| ∈ ℤ
⊢ [a / as][i] = [b / bs][i] ∈ T

2
1. T : Type
2. a : T
3. b : T
4. as : T List
5. bs : T List
6. a = b ∈ T
7. ||as|| = ||bs|| ∈ ℤ
8. p : Sym(||as||)
9. ∀i:ℕ||as||. (as[p.f i] = bs[i] ∈ T)
10. (||as|| + 1) = (||bs|| + 1) ∈ ℤ
11. i : ℕ||as|| + 1
12. ¬((((-1) * i) + ||as||) = ||as|| ∈ ℤ)
⊢ [a / as][1 + (p.f ((-1) + i))] = [b / bs][i] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  a  :  T
3.  b  :  T
4.  as  :  T  List
5.  bs  :  T  List
6.  a  =  b
7.  ||as||  =  ||bs||
8.  p  :  Sym(||as||)
9.  \mforall{}i:\mBbbN{}||as||.  (as[p.f  i]  =  bs[i])
10.  (||as||  +  1)  =  (||bs||  +  1)
11.  i  :  \mBbbN{}||as||  +  1
\mvdash{}  [a  /  as][(||as||  +  1)  -  1  -  if  ((||as||  +  1)  -  1  -  i  =\msubz{}  ||as||)
then  (||as||  +  1)  -  1  -  i
else  ||as||  -  1  -  p.f  (||as||  -  1  -  (||as||  +  1)  -  1  -  i)
fi  ]
=  [b  /  bs][i]


By

---

Latex:
(((SplitOnConclITE  THENA  Auto)  THEN  OnMCls  [0;  -1]  (RW  IntNormC))  THENA  Auto)

---

Home Index