proposition: Lemma states_equiv_tc2a s ss ll : valid_state s -> (forall s : state, In s ss -> valid_state s) -> states_equiv ss ll -> tc2i3 (encode_state s) ll = false -> states_equiv (s :: ss) (tc2a3 (encode_state s) ll).
proof: Proof. intros H H1 H2 H3 l; split; intros H4. - simpl. case (make_listtc2it3 _ _ _ H4). now intros HH; inversion HH. intros (H5, H6). generalize H6; clear H6. case (list3_dec (rev3 l) (encode_state s)); intros H6. now rewrite <- H6, rev3_involutive; auto. rewrite tc2aif3; auto. intros H7; right; unfold states_equiv in H2; rewrite <-H2. now apply make_listtc2ir3; auto. apply encode_valid; auto. - case (list3_dec (rev3 l) (encode_state s)); intros H6. apply make_listtc2ir3; rewrite H6. now apply encode_valid; auto. now apply tc2ai3; auto; apply encode_valid; auto. simpl in H4; case H4; clear H4; intros H4; auto. now case H6; rewrite <- H4, rev3_involutive; auto. unfold states_equiv in H2; rewrite <- H2 in H4. case (make_listtc2it3 _ _ _ H4); auto. now intros HH; inversion HH. intros (H7, H8). apply make_listtc2ir3; auto. rewrite tc2aif3; auto. apply encode_valid; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max