proposition: Lemma enc_characteristic X (s: exp X): normal s -> lambda lambda (var 0) ((ren (shift >> shift) s) (var 1) (var 0)) ≡ lambda lambda (ren (shift >> shift) s) ((var 0) (var 1)) (var 0) -> exists n, s = enc n.
proof: Proof. intros N; apply normal_nf in N as N'. induction N' as [k a t T _ _ isA ->]. intros H'; Injection H'. clear H'. Injection H. clear H. rename H0 into H. asimpl in H. destruct k as [|[|[]]]; cbn in H. - eapply equiv_app_elim in H; (intuition idtac); [|eauto|]. symmetry in H1; eapply equiv_neq_var_app in H1 as []. all: cbn; simplify; destruct a; cbn in isA; eauto. - do 2 (rewrite stepBeta in H; asimpl; trivial). eapply equiv_app_elim in H; (intuition idtac); [|eauto|]. symmetry in H1; eapply equiv_neq_var_app in H1 as []. all: cbn; simplify; destruct a as [[] | | |]; cbn in isA; eauto. - rewrite <-AppR_subst in H. remember (AppR a T) as t. clear isA a T Heqt. do 4 (rewrite stepBeta in H; asimpl; cbn; asimpl; trivial). rewrite idSubst_exp in H; [|intros [|[]]; cbn; eauto]. eapply normal_Lambda in N. pose (sigma := @var X 0 .: var 0 (var 1) .: shift >> (shift >> var)). fold sigma in H. enough (exists n, t = AppL (repeat (var 0) n) (var 1)) as [n ->] by now (exists n). induction t as [[| [|]] | | |]; cbn in H; try solve [unfold funcomp in H; Discriminate]. + exists 0; reflexivity. + eapply head_atom in N as isA; [|eauto]. eapply equiv_app_elim in H as [EQ1 EQ2]; [|eauto|]. 2: eapply atom_head_lifting; trivial. 2: intros [| [| []]]; cbn; eauto. destruct t1 as [[| [|]] | | |]; cbn in EQ1; try Discriminate. * mp IHt2; [eauto using normal_app_r|]. specialize (IHt2 EQ2). destruct IHt2 as [n IHt2]; exists (S n); cbn; now rewrite IHt2. * unfold funcomp in EQ1; Injection EQ1. discriminate. * eapply equiv_neq_var_app in EQ1 as []. eapply atom_head_lifting; trivial. intros [| [| []]]; cbn; eauto. - repeat (rewrite stepBeta in H; cbn; asimpl; trivial). Discriminate. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus second_order.diophantine_equations) Undecidability.HOU.unification(systemunification nth_order_unification)