proposition: Lemma in_states_equiv ss ll s : valid_state s -> (forall s, In s ss -> valid_state s) -> states_equiv ss ll -> in_states s ss = tc2i3 (encode_state s) ll.
proof: Proof. intros Hg Hg1 H. assert (F0: valid3 (rev3 (rev3 (encode_state s)))). rewrite rev3_involutive. now apply encode_valid; auto. generalize (in_states_correct s ss); case in_states; intros H1. assert (F1: In (rev3 (encode_state s)) (tc2it _ make_list nil ll)). unfold states_equiv in H; rewrite H. change (rev3 (encode_state s)) with ((fun x => rev3 (encode_state x)) s). now apply in_map; auto. case (make_listtc2it3 _ _ _ F1). now intros HH; inversion HH. now rewrite rev3_involutive; auto; intros (HH1, HH2); auto. generalize (make_listtc2ir3 ll _ nil F0). rewrite rev3_involutive; auto. case (tc2i3 (encode_state s) ll); auto. unfold states_equiv in H; rewrite H. intros H2; case H1. generalize Hg1 H2; elim ss; simpl; auto; clear ss Hg1 H2 H H1. intros s1 ss Hrec Hg1 Hg2. case (Hg2 (refl_equal true)); intros HH. left. rewrite <- (encode_decode_state s1); auto. rewrite HH, encode_decode_state; auto. right; apply Hrec; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max