proposition: Lemma NT_int_red_subterm_NT_red : forall (R : rules Sig) f, IS (int_red R) f -> exists u, subterm u (f 0) /\ NT (red R) u.
proof: Proof. intros R f hf. subst. ded (hf 0). redtac. destruct c. cong. simpl in xl. clear yr lr cne r. assert (h : forall i, exists v, f i = Fun f0 v). induction i0. fo. clear xl s t0 c t e j i l. destruct IHi0 as [w hw]. ded (hf i0). redtac. destruct c. cong. simpl in xl, yr. rewrite hw in xl. Funeqtac. rewrite yr. exists (Vcast (Vapp t (Vcons (fill c (sub s r)) t0)) e). refl. clear xl s t0 c t e j i l. destruct (choice _ h) as [v hv]. clear h. assert (h : forall i, exists k, exists hk : k < arity f0, int_red_pos_at R k (f i) (f (S i))). intro i. ded (hf i). apply int_red_pos_eq in H. destruct H as [k H]. cut (int_red_pos_at R k (f i) (f (S i))). 2: hyp. intro H'. destruct H as [g [hk [w [e H]]]]. rewrite hv in e. Funeqtac. exists k. exists hk. hyp. destruct (choice _ h) as [k hk]. clear h. set (As := nats_decr_lt (arity f0)). assert (h : forall i, In (k i) As). intro i. destruct (hk i) as [hi ri]. unfold As. rewrite <- In_nats_decr_lt. hyp. destruct (finite_codomain eq_nat_dec h) as [a [g [h1 [h2 h3]]]]. clear h As. assert (ha : a < arity f0). rewrite <- (h2 0). destruct (hk (g 0)). hyp. assert (me : forall x y, x <= y -> g x <= g y). intros x y xy. destruct (lt_dec x y). ded (monS Nat.lt_trans h1). ded (H _ _ l). lia. assert (x=y). lia. subst. refl. assert (hg0 : forall j, j < g 0 -> k j <> a). intros j hj e. destruct (h3 _ e) as [l hl]. subst. destruct (le_dec 0 l). ded (me _ _ l0). lia. lia. assert (hg : forall i j, g i < j < g (S i) -> k j <> a). intros i j hj e. destruct (h3 _ e) as [l hl]. subst. destruct (ge_dec i l). ded (me _ _ g0). lia. destruct (ge_dec l (S i)). ded (me _ _ g0). lia. lia. assert (h0 : Vnth (v 0) ha = Vnth (v (g 0)) ha). cut (forall l, l <= g 0 -> Vnth (v 0) ha = Vnth (v l) ha). intro h. apply h. refl. induction l; simpl. refl. intro h. rewrite IHl. 2: lia. destruct (hk l) as [_ r]. destruct r as [f' [hi [ts [e [w [p1 p2]]]]]]. rewrite hv in e, p2. Funeqtac. Funeqtac. rewrite H, H0. rewrite Vnth_replace_neq. refl. apply (hg0 l). lia. assert (h : forall i, Vnth (v (S (g i))) ha = Vnth (v (g (S i))) ha). intro i. ded (h1 i). cut (forall l, l < g (S i) - g i -> Vnth (v (S (g i))) ha = Vnth (v (S (g i) + l)) ha). intro hi. assert (e : g (S i) = S (g i) + (g (S i) - g i - 1)). lia. rewrite e. apply hi. clear e. clear -H; lia. induction l; intro. rewrite Nat.add_0_r. refl. assert (hl : l < g (S i) - g i). clear -H0; lia. rewrite (IHl hl). rewrite Nat.add_succ_r. simpl. set (x := S (g i + l)). destruct (hk x) as [_ r]. destruct r as [f' [hi [ts [e [w [p1 p2]]]]]]. rewrite hv in e, p2. Funeqtac. Funeqtac. rewrite H1, H2. rewrite Vnth_replace_neq. refl. apply (hg i). unfold x. clear -H0; lia. exists (Vnth (v 0) ha). split. rewrite hv. apply subterm_fun. apply Vnth_in. exists (fun i => Vnth (v (g i)) ha). split. sym. hyp. intro i. rewrite <- h. destruct (hk (g i)) as [_ r]. destruct r as [f' [hi [ts [e [w [p1 p2]]]]]]. rewrite hv in e, p2. Funeqtac. Funeqtac. rewrite H, H0. rewrite Vreplace_pi with (h2:=ha). 2: apply h2. rewrite Vnth_replace. rewrite Vnth_eq with (h2:=hi). 2: sym; apply h2. hyp. Qed.
imports: Coq(IndefiniteDescription ClassicalChoice ProofIrrelevance Lia) CoLoR(RelUtil ATrs LogicUtil ACalls SN InfSeq LeastNat ListUtil BoundNat NatUtil VecUtil ADP NotSN_IS ASN BoolUtil ClassicUtil)