fact: Fixpoint eval_rec5 n t alpha beta ht b := if ieval t b is some v then Pres ht (s2es v) else let score := hget ht t b in let (flag, alpha1, beta1, res1) := if score is Some res then if is_state res then Ares true alpha beta res else if res is drawwin then if beta is edraw then Ares true alpha beta res else Ares false edraw beta res else if alpha is edraw then Ares true alpha beta res else Ares false alpha edraw res else Ares false alpha beta ewin in if flag then Pres ht res1 else if n is n1.+1 then let (ht1, res2) := process_eval_rec5 (eval_rec5 n1 (flip t)) (esflip beta1) (esflip alpha1) ht win (moves t b) in let res3 := if some (esflip res2) == score then edraw else res2 in let ht2 := hput ht1 t b res3 in Pres ht2 res3 else Pres ht edraw.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)