Parcoursup / Calcul de l'ordre d'appel des candidats index
module Pair use int.Int type pair = { i: int; j : int; } let function mkp (i j : int) : pair = { i=i; j=j } predicate in_quadrant (p : pair) = 0 <= p.i < p.j predicate in_quadrant_n (p : pair) (n : int) = 0<= p.i < p.j < n predicate in_rect (p : pair) (ni nj : int) = 0<= p.i < ni && 0<= p.j < nj let function pair_lt (p q : pair) : bool = p.i < q.i || (p.i = q.i && p.j < q.j) let function pair_neq (p q : pair) : bool = p.i <> q.i || p.j <> q.j let function pair_eq (p q : pair) : bool = p.i = q.i && p.j = q.j let lemma mkp_carac (i j :int) ensures { (mkp i j).i = i && (mkp i j).j = j } = () let lemma lt_gt_eq (p q : pair) requires { not pair_lt p q } requires { not pair_lt q p } ensures { pair_eq p q } = () let lemma exists_in_quadrant_n (n : int) : (p : pair) requires { 2 <= n } ensures { in_quadrant_n p n } = assert { exists i j. 0 <= i < j < n }; let i, j = any (i:int, j:int) ensures { 0 <= i < j < n } in mkp i j end (* generated on Thu Jan 30 02:06:23 UTC 2025 from rev: *)
Generated by why3doc 1.7.2+git