proposition: Lemma tot_ext_suc_total A dom (r s: relation A) (ACYC: acyclic r) (SUC: Successor r s) (IN: s ⊆ ⦗fun x => In x dom⦘ ⨾ s ⨾ ⦗fun x => In x dom⦘): is_total (fun x => In x dom) (tot_ext_suc dom r s).
proof: Proof. ins; red; ins. assert (ACYC': acyclic s). by cdes SUC; rewrite INC; done. generalize (last_exists dom ACYC' (dom_helper dom IN IWa)); ins; desc. generalize (last_exists dom ACYC' (dom_helper dom IN IWb)); ins; desc. destruct (classic (b0=b1)) as [EQ1|NEQ1]; subst. - assert (XX: (s＊ ∪ s⁻¹＊) a b). apply functional_path_transp; [apply SUC |]. exists b1; splits. by generalize H; basic_solver. by apply transp_rt with (r:=s); generalize H0; basic_solver. unfold union in XX; desf; apply clos_refl_transE in XX; desf. by left; unfold tot_ext_suc; basic_solver 2. by right; unfold tot_ext_suc; apply transp_ct in XX; basic_solver 2. - assert (tot_ext dom r b0 b1 \/ tot_ext dom r b1 b0); desf. * generalize (tot_ext_total dom r); intro TOT; eapply TOT; try done. + eby eapply dom_helper with (a:=a). + eby eapply dom_helper with (a:=b). * left; red; right. unfold seq in H, H0; desc. do 4 (eexists; splits; eauto). by apply transp_eqv_rel; eauto. by apply transp_rt with (r:=s); generalize H0; basic_solver 2. * right; red; right. unfold seq in H, H0; desc. do 4 (eexists; splits; eauto). by apply transp_eqv_rel; eauto. by apply transp_rt with (r:=s); generalize H0; basic_solver 2. Qed.
imports: Arith micromega.Lia Setoid HahnBase HahnList HahnRelationsBasic HahnEquational HahnRewrite HahnSets HahnMaxElt Zorn