---

Step * of Lemma qexp-qminus

∀n:ℕ. ∀a:ℚ.  (-(a) ↑ n = if isEven(n) then a ↑ n else -(a ↑ n) fi  ∈ ℚ)
BY
{ (InductionOnNat
   THEN Auto
   THEN Try ((RWO "exp_zero_q" 0⋅ THEN Auto))⋅
   THEN RWO "exp_unroll_q" 0⋅
   THEN (Reduce 0 THEN Auto)
   THEN RWO "-2" 0
   THEN Auto
   THEN AutoBoolCase ⌜isEven(n)⌝⋅
   THEN Try ((FLemma `even-implies` [-1] THEN Auto))
   THEN AutoSplit
   THEN Try ((FLemma `even-implies` [-1] THEN Auto))
   THEN QNorm 0
   THEN (InstLemma `odd-or-even` [⌜n⌝]⋅ THENA Auto)
   THEN (RW assert_pushdownC (-1) THENM D -1)
   THEN Auto
   THEN FLemma `odd-implies` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}a:\mBbbQ{}.    (-(a)  \muparrow{}  n  =  if  isEven(n)  then  a  \muparrow{}  n  else  -(a  \muparrow{}  n)  fi  )


By

---

Latex:
(InductionOnNat
  THEN  Auto
  THEN  Try  ((RWO  "exp\_zero\_q"  0\mcdot{}  THEN  Auto))\mcdot{}
  THEN  RWO  "exp\_unroll\_q"  0\mcdot{}
  THEN  (Reduce  0  THEN  Auto)
  THEN  RWO  "-2"  0
  THEN  Auto
  THEN  AutoBoolCase  \mkleeneopen{}isEven(n)\mkleeneclose{}\mcdot{}
  THEN  Try  ((FLemma  `even-implies`  [-1]  THEN  Auto))
  THEN  AutoSplit
  THEN  Try  ((FLemma  `even-implies`  [-1]  THEN  Auto))
  THEN  QNorm  0
  THEN  (InstLemma  `odd-or-even`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENM  D  -1)
  THEN  Auto
  THEN  FLemma  `odd-implies`  [-1]
  THEN  Auto)

---

Home Index