Step * 1 1 of Lemma hd_two_swap_permr


1. Type
2. as List
3. T
4. a' T
5. ((||as|| 1) 1) ((||as|| 1) 1) ∈ ℤ
6. : ℕ(||as|| 1) 1
⊢ [a; [a' as]][swap(0;1) i] [a'; [a as]][i] ∈ T
BY
(AbEval ``swap`` THEN RepeatFor (AutoSplit)) }

1
1. Type
2. as List
3. T
4. a' T
5. ((||as|| 1) 1) ((||as|| 1) 1) ∈ ℤ
6. : ℕ(||as|| 1) 1
7. i ≠ 0
8. 1 ∈ ℤ
⊢ [a'; [a as]][i] ∈ T

2
1. Type
2. as List
3. T
4. a' T
5. ((||as|| 1) 1) ((||as|| 1) 1) ∈ ℤ
6. : ℕ(||as|| 1) 1
7. i ≠ 1
8. i ≠ 0
⊢ [a; [a' as]][i] [a'; [a as]][i] ∈ T


Latex:


Latex:

1.  T  :  Type
2.  as  :  T  List
3.  a  :  T
4.  a'  :  T
5.  ((||as||  +  1)  +  1)  =  ((||as||  +  1)  +  1)
6.  i  :  \mBbbN{}(||as||  +  1)  +  1
\mvdash{}  [a;  [a'  /  as]][swap(0;1)  i]  =  [a';  [a  /  as]][i]


By


Latex:
(AbEval  ``swap``  0  THEN  RepeatFor  2  (AutoSplit))




Home Index