Example (21.1)

　前回の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(ASM_SIMP_TAC[ARITH_RULE`SUC 3 = 4 /\ SUC 1 = 2`; REAL_ARITH`x / &4 = y / &2 <=> x = &2 * y`; REAL_EXP_POS_LT; GSYM LN_POW]);;
e(ASM_SIMP_TAC[TWO; ROOT_LT_LEMMA;]);;
e(FIRST_ASSUM (MP_TAC o GSYM) THEN SIMP_TAC[ARITH_RULE`4 = SUC 3`; ROOT_0; SQRT_0]);;
let root4 = top_thm();;

　&0 = x のときの処理は，相等の対称律を知っているMESONに任せて

e(ASM_MESON_TAC[ARITH_RULE`4 = SUC 3`; ROOT_0; SQRT_0]);;

でもよいのですが，やはりsearchが掛かるので避けました．