proposition: Lemma next2_equiv p ps s ll l : valid_state s -> valid_triple ps -> (forall s1, In s1 (snd ps) -> In s1 (fst (fst ps)) \/ In s1 (snd (fst ps))) -> tstates_equiv ps ll -> state_equiv s l -> tstates_equiv (next2s p ps s) (next2 p ll l).
proof: Proof. unfold next2s, next2. destruct ps as (ss1, ss2). destruct ll as (ll1, ll2). intros Hg Hg1 Hi H1 Hs. simpl in Hg1, Hi, H1. match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => filter2s p ps (f s)) end. match goal with |- context[fold_left ?X ?Y (ll1,?Z)] => replace (fold_left X Y (ll1, Z)) with (fold_left (fun ps f => filter2 p ps (f (decode3 l))) Y (ll1, Z)) end. generalize ss1 ss2 s ll1 ll2 l Hg Hg1 Hi H1 Hs (movel_valid). clear ss1 ss2 s ll1 ll2 l Hg Hg1 Hi H1 Hs. elim movel. now unfold tstates_equiv; simpl; auto. intros f lf Hrec ss1 ss2 s ll1 ll2 l Hg Hg1 Hi H1 Hs Hf. assert (F0: valid_state (f s)); auto with datatypes. repeat rewrite fold_left_cons. case_eq (filter2s p (ss1, ss2) (f s)); intros ss3 ss4 Hss3. case_eq (filter2 p (ll1, ll2) (f (decode3 l))); intros ll3 ll4 Hll3. generalize (filter2_equiv p _ _ _ F0 Hg1 Hi H1). rewrite Hss3. unfold state_equiv in Hs; rewrite Hs, encode_decode_state in Hll3; auto. rewrite Hll3; intros HH; case HH; auto; intros Hf1 (Hf2, Hf3). simpl in Hf1, Hf2, Hf3. apply Hrec; auto with datatypes. now generalize (filter2s_valid p (ss1, ss2) (f s)); rewrite Hss3; intros HH1; case HH1; auto. now generalize (filter2s_incl p (ss1, ss2) (f s)); rewrite Hss3; auto. generalize (ll1, ll2); elim movel; simpl; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max