proposition: Theorem reach11: forall s, reachable s -> nlreachable 11 s.
proof: Proof. native_cast_no_check (iter_final 12). Time Qed. Definition tstates_equiv pss pll := states_equiv (fst (fst pss)) (fst (fst pll)) /\ states_equiv (snd (fst pss)) (snd (fst pll)) /\ states_equiv (snd pss) (snd pll). Definition filter2 pmod (s : (tc2 * tc2) * tc2) l := let ll := encode_state l in let (ps, ns) := s in let (s1, s2) := ps in if (tc2i3 ll s1 || tc2i3 ll s2)%bool then s else match pmod with | xH => ((tc2a3 ll s1,s2), tc2a3 ll ns) | xO _ => ((s1, tc2a3 ll s2), tc2a3 ll ns) | xI _ => ((tc2a3 ll s1, tc2a3 ll s2), tc2a3 ll ns) end. Lemma filter2_equiv p ps ll s : 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 -> tstates_equiv (filter2s p ps s) (filter2 p ll s). Proof. destruct ps as ((ss1, ss2), ss3). destruct ll as ((ll1, ll2), ll3). intros Hg ((Hg1, Hg2), Hg3) Hi (H1, (H2, H3)). simpl in * |-. unfold filter2, filter2s, tstates_equiv. rewrite in_states_equiv with (3 := H1); auto. case_eq (tc2i3 (encode_state s) ll1); simpl fst; simpl snd; auto. rewrite in_states_equiv with (3 := H2); auto. case_eq (tc2i3 (encode_state s) ll2); simpl fst; simpl snd; auto. case p. - intros _ H4 H5; split. now simpl; try apply states_equiv_tc2a; auto. split. now simpl; try apply states_equiv_tc2a; auto. simpl; try apply states_equiv_tc2a; auto. generalize H4 H5. rewrite <- in_states_equiv with (3 := H1); auto. rewrite <- in_states_equiv with (3 := H2); auto. rewrite <- in_states_equiv with (3 := H3); auto. intros H6 H7. generalize (in_states_correct s ss3); case in_states; auto. intros H8; case (Hi _ H8); auto; intros H9; contradict H9. now generalize (in_states_correct s ss1); rewrite H7; auto. generalize (in_states_correct s ss2); rewrite H6; auto. - intros _ H4 H5; split. simpl; try apply states_equiv_tc2a; auto. split. now simpl; try apply states_equiv_tc2a; auto. simpl; try apply states_equiv_tc2a; auto. generalize H4 H5. rewrite <- in_states_equiv with (3 := H1); auto. rewrite <- in_states_equiv with (3 := H2); auto. rewrite <- in_states_equiv with (3 := H3); auto. intros H6 H7. generalize (in_states_correct s ss3); case in_states; auto. intros H8; case (Hi _ H8); auto; intros H9; contradict H9. now generalize (in_states_correct s ss1); rewrite H7; auto. generalize (in_states_correct s ss2); rewrite H6; auto. - intros H4 H5; split. now simpl; try apply states_equiv_tc2a; auto. split. now simpl; try apply states_equiv_tc2a; auto. simpl; try apply states_equiv_tc2a; auto. generalize H4 H5. rewrite <- in_states_equiv with (3 := H1); auto. rewrite <- in_states_equiv with (3 := H2); auto. rewrite <- in_states_equiv with (3 := H3); auto. intros H6 H7. generalize (in_states_correct s ss3); case in_states; auto. intros H8; case (Hi _ H8); auto; intros H9; contradict H9. generalize (in_states_correct s ss1); rewrite H7; auto. generalize (in_states_correct s ss2); rewrite H6; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max