proposition: Theorem free_vars_SSubstAux: ( forall (s : GSym G) (nt : Term s) (sub : SSubstitution vc), disjoint (tBndngVarsDeep vc nt) (rangeFreeVars sub) -> eqset (tfreevars vc (tSSubstAux nt sub)) ( (diff (DeqVtype vc) (ALDom sub) (tfreevars vc nt)) ++ (rangeFreeVars (SubKeepFirst sub (tfreevars vc nt))) ) ) * ( forall (s : GSym G) (pt : Pattern s) (sub : SSubstitution vc), disjoint (pBndngVarsDeep vc pt) (rangeFreeVars sub) -> eqset (pfreevars vc (pSSubstAux pt sub)) ( (diff (DeqVtype vc) (ALDom sub) (pfreevars vc pt)) ++ (rangeFreeVars (SubKeepFirst sub (pfreevars vc pt))) ) ) * ( forall (l : list (bool # GSym G)) (m : Mixture l) (llva : list (list (vType vc))) (sub : SSubstitution vc), disjoint (mBndngVarsDeep vc m ++ (flatten llva)) (rangeFreeVars sub) -> eqset (mfreevars vc (mSSubstAux m llva sub) llva) ( (diff (DeqVtype vc) (ALDom sub) (mfreevars vc m llva)) ++ (rangeFreeVars (SubKeepFirst sub (mfreevars vc m llva))) ) ).
proof: Proof. unfold SubKeepFirst. GInduction; allsimpl; introns Hyp; intros; cpx; try (simpl; rw diff_nil; rw ALKeepFirstNil; simpl; unfold rangeFreeVars, ALRange, ALKeepFirst; simpl; split;cpx);[| | | | ]. - Case "vleaf". rename vc0 into vcc. rewrite DeqSym. destructr (DeqVarSym vc vcc) as [dd|dd]; auto. + destruct dd. allsimpl. rewrite DeqTrue. allunfold ALFindDef. allsimpl. rw diff_cons_r. DALFind Hd;symmetry in HeqHd. * applydup ALFindSome in HeqHd. apply ALInEta in HeqHd0. repnd. apply ALFindSomeKeepFirstSingleton in HeqHd. rw HeqHd. unfold rangeFreeVars; auto. simpl. rw app_nil_r. rw memberb_din. cases_ifd Hd; cpx;[]. rw diff_nil. simpl. unfold eqset. cpx. * applydup ALFindNone in HeqHd. simpl. rewrite DeqTrue. apply ALFindNoneKeepFirstSingleton in HeqHd. rw HeqHd. unfold rangeFreeVars; auto. simpl. rw app_nil_r. rw memberb_din. cases_ifd Hd; cpx;[]. rw diff_nil. unfold eqset. cpx. + rewrite DeqSym. rw <- HeqHdeq. allsimpl. rewrite DeqSym. rw <- HeqHdeq. autorewrite with fast. unfold eqset; cpx. - Case "tnode". unfold allBndngVars. rw <- lBoundVarsSameSSubstAux. apply Hyp. disjoint_reasoning; cpx;[]. SetReasoning. - Case "pnode". apply Hyp. simpl. autorewrite with fast. cpx. - Case "mtcons". destruct llva as [| llh llva]; simpl; cpx; unfold subtractv; allrw diff_app_r; allsimpl. + split. * introv Hin; allrw in_app_iff; dorn Hin; try (apply Hyp0 in Hin); try (apply Hyp in Hin); try(rw in_app_iff in Hin); try(dorn Hin);cpx; try (apply in_diff in Hin); exrepnd; cpx; allsimpl; autorewrite with fast; repeat(disjoint_reasoning);[|]; right; eauto with slow. * introv Hin; allrw in_app_iff. dorn Hin;[dorn Hin;[left|right]|]; try apply Hyp0; try apply Hyp; allrw in_app_iff; allsimpl; autorewrite with fast; repeat(disjoint_reasoning); cpx;[]. apply rangeFreeVarsKeepFirstAppImplies in Hin. dorn Hin;[left|right]; try apply Hyp0; try apply Hyp; allrw in_app_iff;allsimpl; autorewrite with fast; repeat(disjoint_reasoning); cpx; right; cpx. + split. * introv Hin. allrw in_app_iff. dorn Hin;[ | apply Hyp0 in Hin;[|]; repeat (disjoint_reasoning);[]; rw in_app_iff in Hin; dorn Hin; cpx;[]; right; apply rangeFreeVarsKeepFirstAppR; cpx]. rw in_diff in Hin; exrepnd. apply Hyp in Hin0; allrw in_app_iff; exrepnd; allrw in_app_iff;allsimpl; autorewrite with fast; repeat (disjoint_reasoning); unfold SubFilter; try SetReasoning;[| ]. rename l into Hin0. left. left. allrw in_diff; exrepnd; dands; cpx. introv Hc. unfold SubFilter in Hin0. rw <- ALDomFilterCommute in Hin0. allrw in_diff. apply Hin0. dands; cpx. rename l into Hin0. right. apply rangeFreeVarsKeepFirstAppL. SetReasoning. rw ALKeepFirstFilterDiff; auto. * introv Hin. allrw in_app_iff. dorn Hin;[dorn Hin|];[ | | ]. left. allrw in_diff. exrepnd. dands; cpx;[]. unfold SubFilter. apply Hyp. repeat(disjoint_reasoning); SetReasoning. allrw in_app_iff. left. allrw in_diff. exrepnd. dands; cpx;[]. rw <- ALDomFilterCommute. rw in_diff. introv Hc. apply Hin. exrepnd. cpx; fail. allrw in_diff. right. exrepnd; cpx. apply Hyp0;repeat(disjoint_reasoning). allrw in_diff. allrw in_app_iff. allrw in_diff. left; cpx; fail. apply rangeFreeVarsKeepFirstAppImplies in Hin. dorn Hin;[left|right]. allrw in_diff. dands; cpx. apply Hyp;[repeat(disjoint_reasoning); unfold SubFilter; SetReasoning; fail|]. allrw in_app_iff. allrw in_diff. right. SetReasoning. rw ALKeepFirstFilterDiff. eauto. repeat(disjoint_reasoning). apply Hyp3 in X. apply X. SetReasoning; fail. apply Hyp0;repeat(disjoint_reasoning);[]. allrw in_app_iff. allrw in_diff. right. auto. - Case "mpcons". destruct llva as [| llh llva]; simpl; cpx; unfold subtractv; allrw diff_app_r; allsimpl. + split. * introv Hin; allrw in_app_iff; dorn Hin; try (apply Hyp0 in Hin); try (apply Hyp in Hin); try(rw in_app_iff in Hin); try(dorn Hin);cpx; try (apply in_diff in Hin); exrepnd; cpx; allsimpl; autorewrite with fast; repeat(disjoint_reasoning);[|]; right; eauto with slow. * introv Hin; allrw in_app_iff. dorn Hin;[dorn Hin;[left|right]|]; try apply Hyp0; try apply Hyp; allrw in_app_iff; allsimpl; autorewrite with fast; repeat(disjoint_reasoning); cpx;[]. apply rangeFreeVarsKeepFirstAppImplies in Hin. dorn Hin;[left|right]; try apply Hyp0; try apply Hyp; allrw in_app_iff;allsimpl; autorewrite with fast; repeat(disjoint_reasoning); cpx; right; cpx. + split. * introv Hin. allrw in_app_iff. dorn Hin;[ | apply Hyp0 in Hin;[|]; repeat (disjoint_reasoning);[]; rw in_app_iff in Hin; dorn Hin; cpx;[]; right; apply rangeFreeVarsKeepFirstAppR; cpx]. rw in_diff in Hin; exrepnd. apply Hyp in Hin0; allrw in_app_iff; exrepnd; allrw in_app_iff;allsimpl; autorewrite with fast; repeat (disjoint_reasoning); unfold SubFilter;try SetReasoning;[|]. rename l into Hin0. left. left. allrw in_diff; exrepnd; dands; cpx. introv Hc. unfold SubFilter in Hin0. rw <- ALDomFilterCommute in Hin0. allrw in_diff. apply Hin0. dands; cpx. rename l into Hin0. right. apply rangeFreeVarsKeepFirstAppL. SetReasoning. rw ALKeepFirstFilterDiff; auto. * introv Hin. allrw in_app_iff. dorn Hin;[dorn Hin|];[ | | ]. left. allrw in_diff. exrepnd. dands; cpx;[]. apply Hyp. repeat(disjoint_reasoning); unfold SubFilter; SetReasoning. allrw in_app_iff. left. allrw in_diff. exrepnd. dands; cpx;[]. unfold SubFilter. rw <- ALDomFilterCommute. rw in_diff. introv Hc. apply Hin. exrepnd. cpx; fail. allrw in_diff. right. exrepnd; cpx. apply Hyp0;repeat(disjoint_reasoning). allrw in_diff. allrw in_app_iff. allrw in_diff. left; cpx; fail. apply rangeFreeVarsKeepFirstAppImplies in Hin. dorn Hin;[left|right]. allrw in_diff. dands; cpx. apply Hyp;[repeat(disjoint_reasoning); unfold SubFilter;SetReasoning; fail|]. allrw in_app_iff. allrw in_diff. right. SetReasoning. rw ALKeepFirstFilterDiff. eauto. repeat(disjoint_reasoning). apply Hyp3 in X. apply X. SetReasoning; fail. apply Hyp0;repeat(disjoint_reasoning);[]. allrw in_app_iff. allrw in_diff. right. auto. Qed.
imports: Term AssociationList