proposition: Lemma ndRenAlAxAlpha : forall {G : CFGV} {vc : VarSym G} {mp : MixtureParam} (m : Mixture mp) (lln : list (list nat)) (lvA : list (vType vc)), validBsl (length mp) lln -> lAlphaEqAbs (MakeAbstractionsTNodeAux vc lln m) (MakeAbstractionsTNodeAux vc lln (nodeRenAlphaAux lln m lvA)).
proof: Proof. unfold MakeAbstractionsTNodeAux. introv Hv. unfold nodeRenAlphaAux. cases_ifd Hdddd; cpx; eauto with Alpha;[]; clear Hddddf. rewrite <- mLSwapTermEmbedSameLBV. pose proof (renBindersLBVLenSame m (lvA ++ mAllVars m) lln) as Hlen. pose proof (@mRenBindersSpec3 G vc mp m lln (lvA ++ mAllVars m)) as Hnr. apply Hnr in Hv. clear Hnr. pose proof ((mcase (RenBindersSpec vc)) _ m (lvA ++ mAllVars m)) as Hd. simpl in Hd. repnd. clear Hd0. assert ( disjoint (flatten (lBoundVars vc lln (mRenBinders (lvA ++ mAllVars m) m))) (lvA ++ (flatten (lBoundVars vc lln m))) ) as Hld by (apply (subset_disjointLR Hd); auto; [ eauto with SetReasoning | apply subset_app_lr; eauto 2 with SetReasoning]). assert ( disjoint (flatten (lBoundVars vc lln (mRenBinders (lvA ++ mAllVars m) m))) (lvA ++ (mAllVars m)) ) as Had by (apply (subset_disjointLR Hd); eauto with SetReasoning). clear Hd. repeat disjoint_reasoning. clear Had0 Hld0. remember (lBoundVars vc lln m) as lbva. remember (lBoundVars vc lln (mRenBinders (lvA ++ mAllVars m) m)) as lbvb. applydup map_eq_length_eq in Hlen. clear Heqlbvb. clear Heqlbva. remember (lvA ++ mAllVars m) as lv. clear Heqlv. revert lv. generalize dependent lbvb. generalize dependent lbva. clear lln lvA. induction m as [ | ? ? ph ptl Hind| ? ? ph ptl Hind]; cpx. - allsimpl. intros. constructor; cpx. + destruct lbva as [|la lvba]; allsimpl; destruct lbvb as [|lb lbvv]; inverts Hlen0; autorewrite with fast; simpl; [apply AlphaEqNilAbsT; eauto with Alpha; fail|]. pose proof (GFreshDistRenWSpec vc la (tAllVars ph++ (tAllVars (tSwap ph (combine la lb))) ++ la ++lb)) as Hfr. exrepnd. allsimpl. inverts Hlen. apply alAbT with (lbnew:=lvn); try congruence; repeat (disjoint_reasoning); [unfolds_base; simpl; dands; cpx; autorewrite with fast; repeat(disjoint_reasoning); fail |]. rewrite (tcase swap_app). autorewrite with slow; try congruence; cpx; repeat (disjoint_reasoning); eauto with Alpha. + apply Hind; destruct lbva; destruct lbvb; allsimpl; repeat (disjoint_reasoning); inverts Hlen0; inverts Hlen; cpx. - allsimpl. intros. constructor; cpx. + eapply alphaEqTransitive. instantiate (1 := (patAbs vc (lhead lbvb) (pSwap ph (combine (lhead lbva) (lhead lbvb)))) ). * destruct lbva as [|la lvba]; allsimpl; destruct lbvb as [|lb lbvv]; inverts Hlen0; autorewrite with fast; simpl; [apply AlphaEqNilAbsP; eauto with Alpha; fail|]. pose proof (GFreshDistRenWSpec vc la (pAllVars ph++ (pAllVars (pSwap ph (combine la lb))) ++ la ++lb)) as Hfr. exrepnd. allsimpl. inverts Hlen. apply alAbP with (lbnew:=lvn); try congruence; repeat (disjoint_reasoning); [unfolds_base; simpl; dands; cpx; autorewrite with fast; repeat(disjoint_reasoning) |]. rewrite (pcase swap_app). autorewrite with slow; try congruence; cpx; repeat (disjoint_reasoning); eauto with Alpha. * apply AlphaEqNilAbsP. apply alphaEqSym. eapply alphaEqTransitive. instantiate (1 := (pSwap (pRenBinders lv ph) (combine (lhead lbva) (lhead lbvb))) ). apply (pcase (@pAlphaSwapEmSwap G vc)). apply alphaEqSym. apply alphaEquiVariant. apply pRenBindersAlpha. + apply Hind; destruct lbva; destruct lbvb; allsimpl; repeat (disjoint_reasoning); inverts Hlen0; inverts Hlen; cpx. Qed.
imports: AlphaEqProps Omega