needs "../formal_lp/hypermap/main/prove_flyspeck_lp.hl";;


open Flyspeck_lp;;
open Lp_ineqs;;
open Lp_certificate;;
open List_hypermap_computations;;
open List;;
open Lp_informal_computations;;
open Prove_lp;;
open Arith_misc;;
open List_conversions;;
open Lp_main_estimate;;
open Lp_ineqs_proofs;;
open Misc_vars;;

init_ineqs();;


(**************************)

let cert3_file = "/mnt/Repository/formal_lp/glpk/binary/c3.dat";;
let c3 = hd (read_lp_certificates cert3_file);;

let cert4_file = "/mnt/Repository/formal_lp/glpk/binary/c4.dat";;
let c4 = hd (read_lp_certificates cert4_file);;

let cert5_file = "/mnt/Repository/formal_lp/glpk/binary/c5.dat";;
let c5 = hd (read_lp_certificates cert5_file);;

let binary_dir = "/mnt/Repository/formal_lp/glpk/binary";;
let files = map (fun i -> sprintf "%s/c5_%d.dat" binary_dir i) (0--4);;
let cs = map (hd o read_lp_certificates) files;;

let cert = nth cs 4;;
case_info cert.root_case;;
convert_to_list cert.hypermap_string;;
verify_lp_certificate cert;;


let cert = c3;;
let hyp_list = (to_num o create_hol_list o snd o convert_to_list) cert.hypermap_string;;
let base_ineqs, cs = get_terminal_cases cert;;
length cs;;


let th1 = test_terminal (nth cs 4);;
let th2 = INST[`E2:(real^3->bool)->bool`, e_cap_var] th1;;
let th3 = itlist MY_PROVE_HYP base_ineqs th2;;
let th4 = ABBREV_RULE "L" hyp_list th3;;

(****************)

verify_lp_certificate c3;;
verify_lp_certificate c4;;
verify_lp_certificate c5;;

(* 100: 10.671 *)
test 1 (verify_lp_case base_ineqs true) (arg, c4.root_case);;

(* 100: 85.464 *)
test 1 verify_lp_certificate c3;;
(* 100: 10.851 *)
test 1 verify_lp_certificate c4;;
(* 100: 24.318 *)
test 1 verify_lp_certificate c5;;
(* 100: 31.674 *)
test 1 verify_lp_certificate c6;;