Step * 1 1 of Lemma flip-conjugate-rotate


1. : ℕ
2. : ℕ1
3. i ∈ ℕn
4. 1 ∈ ℕn
5. : ℕn
6. rot(n)^i x.if i <then else (x i) fi ) ∈ (ℕn ⟶ ℕn)
7. rot(n)^n x.if (n i) <then (n i) else (x (n i)) fi ) ∈ (ℕn ⟶ ℕn)
⊢ if (x =z i) then 1
if (x =z 1) then i
else x
fi 
(rot(n)^i 
   if (if (n i) <then (n i) else (x (n i)) fi  =z 0) then 1
   if (if (n i) <then (n i) else (x (n i)) fi  =z 1) then 0
   if (n i) <then (n i)
   else (x (n i)) n
   fi )
∈ ℕn
BY
TACTIC:(SplitOnConclITE THENA Auto) }

1
.....truecase..... 
1. : ℕ
2. : ℕ1
3. i ∈ ℕn
4. 1 ∈ ℕn
5. : ℕn
6. rot(n)^i x.if i <then else (x i) fi ) ∈ (ℕn ⟶ ℕn)
7. rot(n)^n x.if (n i) <then (n i) else (x (n i)) fi ) ∈ (ℕn ⟶ ℕn)
8. i ∈ ℤ
⊢ (i 1)
(rot(n)^i 
   if (if (n i) <then (n i) else (x (n i)) fi  =z 0) then 1
   if (if (n i) <then (n i) else (x (n i)) fi  =z 1) then 0
   if (n i) <then (n i)
   else (x (n i)) n
   fi )
∈ ℕn

2
.....falsecase..... 
1. : ℕ
2. : ℕ1
3. i ∈ ℕn
4. 1 ∈ ℕn
5. : ℕn
6. rot(n)^i x.if i <then else (x i) fi ) ∈ (ℕn ⟶ ℕn)
7. rot(n)^n x.if (n i) <then (n i) else (x (n i)) fi ) ∈ (ℕn ⟶ ℕn)
8. ¬(x i ∈ ℤ)
⊢ if (x =z 1) then else fi 
(rot(n)^i 
   if (if (n i) <then (n i) else (x (n i)) fi  =z 0) then 1
   if (if (n i) <then (n i) else (x (n i)) fi  =z 1) then 0
   if (n i) <then (n i)
   else (x (n i)) n
   fi )
∈ ℕn


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  i  :  \mBbbN{}n  -  1
3.  i  \mmember{}  \mBbbN{}n
4.  i  +  1  \mmember{}  \mBbbN{}n
5.  x  :  \mBbbN{}n
6.  rot(n)\^{}i  =  (\mlambda{}x.if  x  +  i  <z  n  then  x  +  i  else  (x  +  i)  -  n  fi  )
7.  rot(n)\^{}n  -  i  =  (\mlambda{}x.if  x  +  (n  -  i)  <z  n  then  x  +  (n  -  i)  else  (x  +  (n  -  i))  -  n  fi  )
\mvdash{}  if  (x  =\msubz{}  i)  then  i  +  1
if  (x  =\msubz{}  i  +  1)  then  i
else  x
fi 
=  (rot(n)\^{}i 
      if  (if  x  +  (n  -  i)  <z  n  then  x  +  (n  -  i)  else  (x  +  (n  -  i))  -  n  fi    =\msubz{}  0)  then  1
      if  (if  x  +  (n  -  i)  <z  n  then  x  +  (n  -  i)  else  (x  +  (n  -  i))  -  n  fi    =\msubz{}  1)  then  0
      if  x  +  (n  -  i)  <z  n  then  x  +  (n  -  i)
      else  (x  +  (n  -  i))  -  n
      fi  )


By


Latex:
TACTIC:(SplitOnConclITE  THENA  Auto)




Home Index