---

Step * 1 of Lemma exp-minusone

.....upcase..... 
1. n : ℤ
2. 0 < n
3. -1^n - 1 = if ((n - 1) mod 2 =z 0) then 1 else -1 fi  ∈ ℤ
⊢ -1^n = if (n mod 2 =z 0) then 1 else -1 fi  ∈ ℤ
BY
{ (Unfold `exp` 0
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN OldAutoBoolCase ⌜(n =z 0)⌝⋅
   THEN Fold `exp` 0
   THEN Auto
   THEN (HypSubst' (-2) 0)
   THEN (Thin (-2))
   THEN ((InstLemma `add-one-mod-2` [⌜n - 1⌝])⋅ THENA Auto)
   THEN (Subst' (n - 1) + 1 ~ n -1 THENL [Auto; HypSubst' -1 0])
   THEN ((InstLemma `mod_bounds` [⌜n - 1⌝; ⌜2⌝])⋅ THENA Auto)
   THEN (MoveToConcl (-1))
   THEN (GenConclAtAddr [1; 1; 2])
   THEN Auto) }

---

Latex:

---

Latex:
.....upcase..... 
1.  n  :  \mBbbZ{}
2.  0  <  n
3.  -1\^{}n  -  1  =  if  ((n  -  1)  mod  2  =\msubz{}  0)  then  1  else  -1  fi 
\mvdash{}  -1\^{}n  =  if  (n  mod  2  =\msubz{}  0)  then  1  else  -1  fi 


By

---

Latex:
(Unfold  `exp`  0
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  OldAutoBoolCase  \mkleeneopen{}(n  =\msubz{}  0)\mkleeneclose{}\mcdot{}
  THEN  Fold  `exp`  0
  THEN  Auto
  THEN  (HypSubst'  (-2)  0)
  THEN  (Thin  (-2))
  THEN  ((InstLemma  `add-one-mod-2`  [\mkleeneopen{}n  -  1\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -1  THENL  [Auto;  HypSubst'  -1  0])
  THEN  ((InstLemma  `mod\_bounds`  [\mkleeneopen{}n  -  1\mkleeneclose{};  \mkleeneopen{}2\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;  1;  2])
  THEN  Auto)

---

Home Index