４変数から３変数の場合を導きましょう．まず，lemmaを用意します． g`!x. &0 <= x ==> root 3 x = root 4 ( root 3 x * x )`;; e(SIMP_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC);; e(ASM_SIMP_TAC[ARITH_RULE`3 = SUC 2 /\ 4 = SUC 3`; REAL_EXP_POS_LT; REA…

前回のroot4をexpを用いて証明してみます． g`!x. &0 <= x ==> root 4 x = sqrt( sqrt x )`;; e(SIMP_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC);; e(ASM_SIMP_TAC[sqrt; ARITH_RULE`4 = SUC 3 /\ 2 = SUC 1`; ROOT_LN; REAL_EXP_POS_LT; REAL_EXP_INJ]);; e(A…