proposition: Lemma chain_min_fun : forall f, defined f R = true -> forall ts, SN chain_min (Fun f ts) -> Vforall SNR ts -> SNR (Fun f ts).
proof: Proof. cut (forall t, SN chain_min t -> forall f, defined f R = true -> forall ts, t = Fun f ts -> Vforall SNR ts -> SNR t). intros. apply H with (f := f) (ts := ts); (hyp || refl). intros t H. elim H. clear t H. intros t H IH f H0 ts H1 Hsnts. assert (SN (Vrel1 (red R)) ts). apply Vforall_SN_rel1. hyp. gen IH. rewrite H1. elim H2. clear IH ts H1 Hsnts H2. intros ts H1 IH1 IH2. assert (Hsnts : Vforall SNR ts). apply SN_rel1_forall. apply SN_intro. hyp. clear H1. assert (H1 : forall y, Vrel1 (red R) ts y -> SNR (Fun f y)). intros. apply IH1. hyp. intros. eapply IH2. eapply gt_chain_min. apply H1. trivial. apply H2. apply H3. apply H4. hyp. clear IH1. apply SN_intro. intros u H2. redtac. destruct c; simpl in xl, yr. destruct (fun_eq_sub xl). destruct e as [ls]. rewrite H2, sub_fun in xl. Funeqtac. assert (Hsnsx : forall x, In x (vars l) -> SNR (s x)). intros. eapply sub_fun_sn with (f := f). subst l. apply H4. rewrite H3 in Hsnts. exact Hsnts. subst u. assert (r = sub (alien_sub r) (cap r)). apply sym_eq. apply (alien_sub_cap R). rewrite H4, sub_sub. apply no_call_sub_sn. hyp. apply calls_cap. intros. ded (vars_cap R H5). case (le_lt_dec x (maxvar r)); intro; unfold sub_comp, ACap.alien_sub. ded (vars_cap_inf R H5 l0). ded (hyp2 lr _ H7). rewrite fsub_inf. simpl. apply Hsnsx. hyp. hyp. rewrite (fsub_nth (aliens (capa r)) l0 H6). set (a := Vnth (aliens (capa r)) (lt_pm (k:=projT1 (capa r)) l0 H6)). assert (Fun f ts = sub s l). rewrite H3, H2. refl. assert (In a (calls R r)). apply aliens_incl_calls. unfold a. apply Vnth_in. ded (in_calls H8). destruct H9 as [g]. destruct H9 as [vs]. destruct H9. eapply calls_sn with (r := r). hyp. intros. apply Hsnsx. apply (hyp2 lr _ H11). intros h ws H13 H14. case_eq (negb_subterm l (Fun h ws)); intros. rename H11 into z. apply IH2 with (y := Fun h (Vmap (sub s) ws)) (f := h) (ts := Vmap (sub s) ws). unfold chain_min. split. rewrite H7, <- sub_fun. eapply in_calls_chain. apply lr. hyp. hyp. split. simpl. apply Vforall_lforall. trivial. simpl. apply Vforall_lforall. trivial. eapply in_calls_defined. apply H13. refl. hyp. revert H11. unfold negb_subterm. rewrite negb_lr. simpl negb. rewrite bsubterm_ok. intro H11. rewrite H2 in H11. destruct (subterm_fun_elim H11). destruct H12. apply subterm_eq_sn with (t := sub s x0). eapply Vforall_in. apply Hsnts. rewrite H3. apply Vin_map_intro. hyp. apply subterm_eq_sub. hyp. hyp. decomp e. subst l. is_var_lhs. Funeqtac. subst u. apply H1. rewrite H2. apply Vrel1_cast_intro. apply Vrel1_app_intro_l. apply Vrel1_cons_intro. left. split. eapply red_rule. hyp. refl. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)