proposition: Lemma firstorder_decidable' (I: orduni 1 X): ord' Gamma₀ <= 1 -> ord A₀ <= 2 -> normal s₀ -> normal t₀ -> Dec (NOU 1 I).
proof: Proof. intros O1 O2 N1 N2; eapply iff_dec with (P := exists Delta sigma, Delta ⊩(1) sigma : Gamma₀ /\ sigma • s₀ = sigma • t₀ /\ (forall x : fin, normal (sigma x))). split; intros (Delta & sigma & ?); exists Delta; exists sigma; intuition idtac; eauto 2 using FO_subst_equiv_eq, eq_equiv. destruct I as [Gamma s t A H1 H2]; cbn in *; subst. unfold NOU; cbn in *. eapply normal_nf in N1 as N1'; destruct N1' as [k1 s ? ? ? ? ->]. eapply normal_nf in N2 as N2'; destruct N2' as [k2 t ? ? ? ? ->]. eapply normal_Lambda in N1. eapply normal_Lambda in N2. destruct (k1 == k2) as [H4|H4]; [subst; destruct (@unif _ (fun x => x >= k2) _ [(AppR s T, AppR t T0)]) as [[sigma H']|H']|]. 1: left. 2: right. 3: right. all: eapply Lambda_ordertyping_inv in H1 as (L & B & ? & ? & ?). all: eapply Lambda_ordertyping_inv in H2 as (L' & B' & ? & ? & ?); subst. 1, 2: assert (L = L' /\ B = B') as []; [|subst L' B'; clear H3 H4]. 1, 3: try (clear H'); eapply Arr_inversion in H3 as [? []]; try lia; rewrite ?H4; eauto 2; destruct x; cbn in *; simplify in H0; eauto 2; subst; simplify in H4; cbn in H4; lia. all: simplify in O2; cbn in O2; destruct O2 as [O2 _]; eapply le_S_n in O2. all: assert (ord' (rev L ++ Gamma) <= 1) by now simplify. all: eapply order_one_lambda_free in N1 as L1; simplify; eauto 2. all: eapply order_one_lambda_free in N2 as L2; simplify; eauto 2. + eapply unify_free' in H' as P. eapply unify_typing with (Gamma := rev L ++ Gamma) (L := [B]) in H' as T2; [| eauto|simplify; cbn; intuition idtac; eauto using all_terms_nil|eauto using eqs_ordertyping]. specialize (unify_lambda_free H') as LF; mp LF; simplify; intuition idtac; eauto using all_terms_nil. exists Gamma. exists (decr (length L) sigma). intuition idtac. * specialize decr_typing with (L := rev L) as H9; simplify in H9; eauto. * eapply decr_unifies; eauto. specialize (unify_unifiable H' (AppR s T, AppR t T0)); cbn; auto. * eapply lambda_free_normal. pose proof (free := fun (k: nat) (x: nat) => x >= k). eapply decr_lambda_free; intros; eapply LF. + intros (Delta & sigma & E1 & E2 & E3). asimpl in E2. eapply Lambda_injective in E2. edestruct unify_complete with (sigma := it (|L|) up sigma) (E := [(AppR s T,AppR t T0)]) (free := free (|L|)); eauto. * typeclasses eauto. * eapply it_up_free'. * rewrite Unifies_cons. cbn; unfold unifies; asimpl; asimpl in E2; intuition eauto using Unifies_nil. * simplify; eauto using all_terms_nil. + intros (Delta & sigma & ? & ? & ?). assert (|L| < |L'| \/ |L'| < |L|) as [LT|LT] by lia. 2: symmetry in H3. all: eapply Arr_inversion in H3 as [L'']. 2,4:intuition auto. all:intuition idtac;subst. all: simplify in H5; asimpl in H5; rewrite <-Lambda_plus in H5. all: eapply Lambda_injective in H5; destruct L''; [ simplify in LT; try lia; cbn in H5 | ]. 1: destruct T; destruct s; cbn in H5; try discriminate; [| destruct i]. 2: destruct T0; destruct t; cbn in H5; try discriminate; [| destruct i0]. all: try destruct (le_lt_dec (length L') f); try destruct (le_lt_dec (length L) f). 2, 4: rewrite it_up_lt in H5; try discriminate;eauto 2. 1: inv H. 2: inv H2. all: cbn [Arr] in H7; now eapply ord_arr_one in H7. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)