proposition: Lemma MU_PCP S': NOU 3 (PCP_to_U S') -> PCP S'.
proof: Proof. intros (Delta & sigma & T & H & N); cbn in *. repeat apply equiv_lam_elim in H. eapply equiv_app_elim in H as [EQ2 EQ1]; cbn; intuition idtac. eapply equiv_app_elim in EQ2 as [_ EQ2]; cbn; intuition idtac. rewrite !AppR_subst in EQ1; rewrite !AppR_subst in EQ2. rewrite !Enc_subst_id in EQ2;try reflexivity. cbn in *. unfold funcomp in *. rewrite !ren_plus_base, !ren_plus_combine in *; change (1 + 1 + 1) with 3 in *. unfold shift, var_zero in *. rewrite map_id_list in EQ1; [| intros ? ? % repeated_in; now subst ]. assert (Delta ⊢(3) sigma 0 : Arr (repeat (alpha → alpha) (length S')) alpha) as T1 by now apply T. specialize (N 0) as N2; eapply normal_nf in N2 as N3. destruct N3 as [k x t' T' Hi H ->]. eapply Lambda_ordertyping_inv in T1 as (L & B & H0 & H1 & <-). eapply id in H0 as T2. assert (|L | <= |S'|) as L1 by (eapply (f_equal arity) in H1; simplify in H1; rewrite H1; trivial). symmetry in H1; eapply Arr_inversion in H1 as (L2 & H1 & H2); simplify; trivial. eapply repeated_app_inv in H1 as (H1 & H3 & H4); trivial. rewrite H4 in H2; subst B. rewrite H3 in *; simplify in *. clear H3 H4 L1. revert H0 H1 EQ1 EQ2 T2 N2. generalize (length L); generalize (length L2); clear L L2. intros l k H0 H1 EQ1 EQ2 T2 N2. edestruct (@list_decompose_alt k _ S') as (S1 & S2 & H4 & H5); [lia|]; subst S'. rewrite !Lambda_ren in EQ1; rewrite !Lambda_ren in EQ2. simplify in EQ1 EQ2; rewrite !AppR_app in EQ1; rewrite !AppR_app in EQ2. simplify in H1; assert (length S1 = l) as H2 by lia; clear H1; subst. rewrite !AppR_Lambda' in EQ1, EQ2; simplify; trivial. rewrite AppR_Lambda' in EQ2; simplify; trivial. rewrite it_up_var_sapp in EQ1; simplify; intros; [|lia..]. rewrite !it_up_var_sapp in EQ2; simplify; intros; [|lia..]. destruct (AppL_decomposition (AppR x T') (|S2|)) as [[I t] (H1&H2&H3)]. rewrite H2 in EQ1, EQ2. destruct S1. + rewrite H2 in *. assert (normal t) by now eapply normal_AppL_right, normal_Lambda. rewrite !AppL_subst in EQ1; rewrite !AppL_subst in EQ2. cbn -[add] in *. rewrite !select_variables_subst in EQ2. rewrite !select_variables_subst in EQ1. 2 - 4: simplify; (auto 2). rewrite <-!select_map, !enc_concat in EQ2. eapply AppL_ordertyping_inv in T2 as (L' & B & H8 & H9). eapply enc_eq in EQ2; trivial. 2 - 3: split; intros EQ3; eapply end_is_var_typed in EQ3 as (? & ? & ? & ?); cbn; simplify. 6, 9, 15, 21 : easy. 3, 8, 13, 16 : now eauto 1. 2, 6, 10, 13: eapply H3; cbn; (eauto 1); cbn; now simplify in *. 3, 5, 8, 11: now auto. 3, 5, 9: now eauto. 3, 4, 6: now auto. 2 - 3: intros; cbn; unfold funcomp, u, v; intuition discriminate. exists I; intuition idtac. 2: rewrite <-!select_map; (auto 2). subst; cbn [map select concat AppL] in H6, EQ1. eapply end_is_var in EQ1 as (? & ? & ? & ?); trivial. eapply H3; cbn; (eauto 1); cbn; now simplify in *. intros; cbn; (intuition idtac); discriminate. intros ? ? % repeated_in; subst; easy. + eapply id in T2 as T3. eapply AppR_ordertyping_inv in T2 as (L' & T2 & T4). destruct x as [i | | |]; cbn in H; [| |easy..]. * inv T4. assert (i < length S2 \/ i >= length S2) as [H42|H42] by lia. ** rewrite nth_error_app1, nth_error_repeated in H6; simplify; trivial. injection H6 as H6. eapply (f_equal ord) in H6. simplify in H6. symmetry in H6; eapply Nat.eq_le_incl in H6. clear - H6. simplify in H6. cbn in H6. lia. ** rewrite <-H2 in EQ1. asimpl in EQ1. rewrite sapp_ge_in in EQ1; simplify; (auto 2). eapply equiv_head_equal in EQ1; simplify; cbn; (auto 2). simplify in EQ1; cbn in EQ1. discriminate EQ1. * rewrite <-H2 in EQ1. exfalso. asimpl in EQ1. eapply equiv_head_equal in EQ1; cbn; simplify; cbn; trivial. cbn in EQ1; simplify in EQ1; discriminate. Qed.
imports: RelationClasses Morphisms List Arith Lia Init.Nat Setoid Undecidability.HOU(std.std calculus.calculus unification.unification) Undecidability.HOU(third_order.pcp third_order.encoding)