---

Step * 2 1 2 1 1 1 1 1 of Lemma rotate-as-flips


1. n : ℤ
2. 0 < n
3. flips : (ℕn - 1 × ℕn - 1) List
4. ¬(n = 1 ∈ ℤ)
5. x : ℕn
⊢ if ((n - 2, n - 1) x =z n - 1) then (n - 2, n - 1) x else compose-flips(flips) ((n - 2, n - 1) x) fi 
= (compose-flips(flips @ [<n - 2, n - 1>]) x)
∈ ℕn
BY
{ Assert ⌜(compose-flips(flips @ [<n - 2, n - 1>]) x) = (compose-flips(flips) ((n - 2, n - 1) x)) ∈ ℕn⌝⋅ }

1
.....assertion..... 
1. n : ℤ
2. 0 < n
3. flips : (ℕn - 1 × ℕn - 1) List
4. ¬(n = 1 ∈ ℤ)
5. x : ℕn
⊢ (compose-flips(flips @ [<n - 2, n - 1>]) x) = (compose-flips(flips) ((n - 2, n - 1) x)) ∈ ℕn

2
1. n : ℤ
2. 0 < n
3. flips : (ℕn - 1 × ℕn - 1) List
4. ¬(n = 1 ∈ ℤ)
5. x : ℕn
6. (compose-flips(flips @ [<n - 2, n - 1>]) x) = (compose-flips(flips) ((n - 2, n - 1) x)) ∈ ℕn
⊢ if ((n - 2, n - 1) x =z n - 1) then (n - 2, n - 1) x else compose-flips(flips) ((n - 2, n - 1) x) fi 
= (compose-flips(flips @ [<n - 2, n - 1>]) x)
∈ ℕn

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  flips  :  (\mBbbN{}n  -  1  \mtimes{}  \mBbbN{}n  -  1)  List
4.  \mneg{}(n  =  1)
5.  x  :  \mBbbN{}n
\mvdash{}  if  ((n  -  2,  n  -  1)  x  =\msubz{}  n  -  1)
then  (n  -  2,  n  -  1)  x
else  compose-flips(flips)  ((n  -  2,  n  -  1)  x)
fi 
=  (compose-flips(flips  @  [<n  -  2,  n  -  1>])  x)


By

---

Latex:
Assert  \mkleeneopen{}(compose-flips(flips  @  [<n  -  2,  n  -  1>])  x)  =  (compose-flips(flips)  ((n  -  2,  n  -  1)  x))\mkleeneclose{}\mcdot{}

---

Home Index