proposition: Lemma FIB_HI x y : i_P x y -> (exists s t, s/t el R /\ x = ienc s /\ y = ienc t) \/ (exists s t u v, s/t el R /\ x = iprep s u /\ y = iprep t v /\ i_P u v /\ ((sub u x /\ v = y) \/ (sub v y /\ u = x) \/ (sub u x /\ sub v y))).
proof: Proof. destruct x as [ [x HX]|], y as [ [y HY]|]; cbn; auto. induction 1. - left. exists x, y. repeat setoid_rewrite obstring_ienc. repeat split; trivial. - assert (HU : |u| <= n). { rewrite app_length in HX. lia. } assert (HV : |v| <= n). { rewrite app_length in HY. lia. } destruct x as [|b x], y as [|c y]. + cbn. apply IHderivable. + right. exists [], (c::y), (obcast HU), (obcast HV). repeat setoid_rewrite obstring_iprep. repeat split; trivial. right. left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq. + right. exists (b::x), [], (obcast HU), (obcast HV). repeat setoid_rewrite obstring_iprep. repeat split; trivial. left. repeat split; eauto using app_neq. f_equal. now apply bstring_eq. + right. exists (b::x), (c::y), (obcast HU), (obcast HV). repeat setoid_rewrite obstring_iprep. repeat split; trivial. right. right. repeat split; eauto using app_neq. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation