proposition: Lemma filter_equiv ps ll s : valid_state s -> valid_pair ps -> incl (snd ps) (fst ps) -> pstates_equiv ps ll -> pstates_equiv (filters ps s) (filter ll s).
proof: Proof. destruct ps as (ss1, ss2). destruct ll as (ll1, ll2); simpl. intros Hg (Hg1, Hg2) Hi (H1, H2). simpl in H1, H2. unfold filter, filters, pstates_equiv. rewrite in_states_equiv with (3 := H1); auto. case_eq (tc2i3 (encode_state s) ll1); simpl fst; simpl snd; auto. split; apply states_equiv_tc2a; auto. generalize H. rewrite <- in_states_equiv with (3 := H1); auto. rewrite <- in_states_equiv with (3 := H2); auto. intros HH. generalize (in_states_correct s ss1); rewrite HH; intros HH1. generalize (in_states_correct s ss2); case in_states; auto. intros HH2; case HH1; auto with datatypes. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max