val max: x:int -> y:int -> Tot (z:int{ (x >= y ==> z = x) /\ (x < y ==> z = y) })
let max x y = if x >= y then x else y
val max: x:int -> y:int -> Tot (z:int{ (x >= y ==> z = x) /\ (x < y ==> z = y) })
let max x y =
if x >= y then x else y
FStar.Math.Lib.fst.checked
prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
FStar.Math.Lib.fst
Prims.int Prims.op_GreaterThanOrEqual Prims.bool Prims.l_and Prims.l_imp Prims.b2t Prims.op_Equality Prims.op_LessThan
(*
   Copyright 2008-2018 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)
module FStar.Math.Lib

open FStar.Mul

(* Definition of the division operator *)
val lemma_div_def: a:nat -> b:pos -> Lemma (a = b * (a/b) + a % b)
let lemma_div_def a b = ()

private let mul_lemma (a:nat) (b:nat) (c:nat) : Lemma (requires (a <= b))
                                           (ensures  (c * a <= c * b))
  = ()

private let mul_lemma' (a:nat) (b:nat) (c:pos) : Lemma (requires (c * a <= c * b))
                                           (ensures (a <= b))
  = ()

private let mul_div_lemma (a:nat) (b:pos) : Lemma (b * (a / b) <= a) = ()

val slash_decr_axiom: a:nat -> b:pos -> Lemma (a / b <= a)
let slash_decr_axiom a b =
    mul_lemma 1 b a;
    mul_div_lemma a b;
    mul_lemma' (a / b) a b

private let lemma_mul_minus_distr_l (a:int) (b:int) (c:int) : Lemma (a * (b - c) = a * b - a * c)
  = ()

(* Axiom: definition of the "b divides c" relation *)
#reset-options "--z3rlimit 30"
val slash_star_axiom: a:nat -> b:pos -> c:nat -> Lemma
  (requires (a * b = c))
  (ensures  (a = c / b))
let slash_star_axiom a b c =
  lemma_div_def c b;
  lemma_mul_minus_distr_l b a (c/b)

#reset-options
val log_2: x:pos -> Tot nat
let rec log_2 x =
  if x >= 2 then 1 + log_2 (x / 2) else 0

(* Function: power of x *)
val powx : x:int -> n:nat -> Tot int
let rec powx x n =
  match n with
  | 0 -> 1
  | n -> x * powx x (n - 1)

(* Function: absolute value *)
val abs: x:int -> Tot (y:int{ (x >= 0 ==> y = x) /\ (x < 0 ==> y = -x) })
let abs x = if x >= 0 then x else -x

(* Function: maximum value *)
val max: x:int -> y:int -> Tot (z:int{ (x >= y ==> z = x) /\ (x < y ==> z = y) })
x: Prims.int -> y: Prims.int -> z: Prims.int{(x >= y ==> z = x) /\ (x < y ==> z = y)}