proposition: Lemma process_eval_rec3_correct (res beta : state) l : alpha < beta -> alpha <= beta <= res -> let res1 := \smin_(i <- l) f1 i in let res2 := process_eval_rec3 f2 alpha beta res l in alpha <= res1 <= beta -> res2 = sflip res1.
proof: Proof. elim: l res beta => [|i l IH] res beta aLsb /andP[aLb bLr]; lazy zeta. rewrite big_nil => /andP[_ /ge_winE rEwin]. by move: bLr; rewrite rEwin => /ge_winE->. rewrite big_cons /= => H; have /andP[H1 H2] := H. have [E1|E1] := leqP res _. have [E2|/ltnW E2] := leqP (\smin_(j <- l) f1 j) (f1 i). rewrite smin_ler // in H H1 H2 *. by apply: IH => //; rewrite aLb. rewrite smin_lel // in H H1 H2 *. rewrite f1H // in E1. have f1E : f1 i = beta by apply: sle_antisym => //; apply: leq_trans E1. rewrite f1E in E1 E2 H1 H2 *. have rE : res = beta by apply: sle_antisym. rewrite rE. apply: sle_antisym; last first. by rewrite ge_process_eval_rec3. by apply: process_eval_rec3_correct_b E2; rewrite aLsb leqnn. have [E2|E2] := leqP beta _. have [E3|/ltnW E3] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H H1 H2 *. rewrite f1H // in E1 E2 *. apply: sle_antisym; last first. by rewrite ge_process_eval_rec3. have -> : f1 i = beta by apply: sle_antisym. apply: process_eval_rec3_correct_b (leq_trans E2 E3) => //. by rewrite aLsb leqnn. rewrite smin_ler // in H H1 H2 *. by rewrite IH // aLb. have [E3|E3] := leqP (f2 _ _ _) alpha => //. have [E4|E4] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite (smin_lel E4) in H H1 H2 *. by rewrite (f1H aLsb H). rewrite smin_ler // in H H1 H2 *; last by apply: ltnW. have H3 : alpha < f1 i by apply: leq_ltn_trans H1 E4. have H4 : alpha <= f1 i by apply: ltnW. have [E5|E5] := leqP (f1 i) beta. have H4E5 : alpha <= f1 i <= beta by rewrite H4. rewrite (f1H aLsb H4E5) in E1 E2 E3 *. by rewrite ltnNge in H3; case/negP: H3. rewrite ltnNge in E2; case/negP: E2. by apply: f1Hb; rewrite // aLsb /= ltnW. have [E4|E4] := leqP (f1 i) (\smin_(j <- l) f1 j). rewrite smin_lel // in H H1 H2 *. rewrite (f1H aLsb H) in E1 E2 E3 *. apply: sle_antisym; last by rewrite ge_process_eval_rec3. apply: process_eval_rec3_correct_b E4 => //. by rewrite E3 leqnn. rewrite smin_ler // in H H1 H2 *; last by apply: ltnW. have [E5|E5] := leqP (f1 i) beta. have H3 : alpha < f1 i by apply: leq_ltn_trans H1 E4. have H4 : alpha <= f1 i by apply: ltnW. have H4E5 : alpha <= f1 i <= beta by rewrite H4. rewrite (f1H aLsb H4E5) in E1 E2 E3 *. rewrite IH //; last by rewrite H1 ltnW. by rewrite (ltnW E3) leqnn. rewrite ltnNge in E2; case/negP: E2. by apply: f1Hb; rewrite // aLsb ltnW. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)