proposition: Theorem O1_count_Oi_eq_until_bad : forall s s_A, comp_spec (fun a b => ((snd (snd a) > q) <-> (snd (snd b) > q)) /\ ((snd (snd a) <= q)%nat -> (fst a = fst b /\ fst (snd a) = fst (snd b)))) ((A1 s_A) _ _ O1_count (s, 0)%nat) ((A1 s_A) _ _ (Oi q) (s, 0)%nat).
proof: Proof. intuition. eapply comp_spec_consequence. eapply (fcf_oracle_eq_until_bad (fun x => if (gt_dec (snd x) q) then true else false) (fun x => if (gt_dec (snd x) q) then true else false) eq); intuition; subst. apply O1_count_wf. apply Oi_wf. pairInv. unfold O1_count, Oi. destruct (ge_dec b1 q). fcf_irr_l. fcf_irr_r. fcf_simp. fcf_spec_ret; simpl in H2; destruct (gt_dec (S b1) q); try discriminate; try lia. fcf_skip. fcf_spec_ret; intuition. apply O1_count_increases in H0. simpl in *. fcf_compute. apply Oi_count_increases in H0. simpl in *. fcf_compute. intuition; simpl in *. fcf_compute. destruct (gt_dec b1 q); trivial. destruct (gt_dec (snd (snd b0)) q); intuition; discriminate. destruct (gt_dec b1 q). lia. intuition. destruct b0. destruct (gt_dec b1 q). lia. intuition. simpl in *. subst. trivial. Qed.
imports: FCF.FCF FCF.RndInList