sqrt_scaf: THEORY BEGIN e: VAR posreal x, y: VAR real epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y px, py: VAR nonneg_real times_pos_lt1: LEMMA px * py < 1 => px < 1 OR py < 1 times_pos_le1: LEMMA px * py <= 1 => px <= 1 OR py <= 1 times_pos_gt1: LEMMA px * py > 1 => px > 1 OR py > 1 times_pos_ge1: LEMMA px * py >= 1 => px >= 1 OR py >= 1 ge1_square_ge: LEMMA 1 <= px => px <= px * px i: var posnat expt_0: lemma 0^i = 0 ge1_expt_ge: LEMMA 1 <= px => px <= px ^ i lt1_expt_le: LEMMA px<1 => px^i <= px square_def: LEMMA x^2 = x*x expt_pos_le: LEMMA px^i<=py^i <=> px<=py expt_pos_lt: LEMMA px^i pxpy^i <=> px>py expt_pos_ge: LEMMA px^i>=py^i <=> px>=py sqrt_exists: LEMMA EXISTS (x1: [px: nonneg_real -> {py | py ^ 2 = px}]): TRUE; sqrt(px): {py | py^2 = px} sqrt1: lemma sqrt(px^2)=px sqrt_abs: lemma sqrt(x^2) = abs(x) END sqrt_scaf