4 !x n. x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0 [1]
9 ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0) [2]
12 qed by ASM_REWRITE_TAC[real_pow],3;
14 ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) \/ n = 0) [4]
17 abs x = &1 ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n)) [6]
19 assume abs x = &1 [7];
20 &1 < &0 ==> EVEN n [8] by REAL_ARITH_TAC,5;
21 &1 pow n = &1 <=> &1 < &0 ==> EVEN n [9]
22 by ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE],5 from 8;
23 EVEN n ==> (&1 = &1 <=> -- &1 < &0 ==> T) [10]
26 qed by ASM_REWRITE_TAC[],5,11;
27 ~EVEN n ==> (-- &1 = &1 <=> -- &1 < &0 ==> F) [12]
30 -- &1 = &1 <=> ~(-- &1 < &0) [14] by REAL_ARITH_TAC,5,13;
31 qed by ASM_REWRITE_TAC[],5,13 from 14;
32 (if EVEN n then &1 else -- &1) = &1 <=> -- &1 < &0 ==> EVEN n [15]
33 by REPEAT COND_CASES_TAC,5 from 10,12;
34 -- &1 pow n = &1 <=> -- &1 < &0 ==> EVEN n [16]
35 by ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE],5 from 15;
36 x pow n = &1 <=> x < &0 ==> EVEN n [17]
37 by FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (REAL_ARITH (parse_term "abs x = a ==> x = a \\/ x = --a"))),5,7
39 x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n) [18]
40 by ASM_REWRITE_TAC[],5,7 from 17;
41 qed by ALL_TAC,5,7 from 18;
43 ==> (x pow n = &1 <=> abs x = &1 /\ (x < &0 ==> EVEN n)) [19]
45 assume ~(abs x = &1) [20];
46 qed by ASM_MESON_TAC[REAL_POW_EQ_1_IMP],5,20;
48 :: 2: inference time-out
49 qed by ASM_REWRITE_TAC[real_pow],5 from 18;
52 qed by ASM_CASES_TAC (parse_term "n = 0") from 2,4;`;;