proposition: Lemma iter2_final n : let (ps,s3) := iter2 n in let (s1,s2) := ps in match s3 with OTC2 => (forall s, reachable s -> tc2i3 (encode_state s) s1 = true \/ tc2i3 (encode_state s) s2 = true) /\ (forall s, valid_state s -> tc2i3 (encode_state s) s1 = true -> exists m1, (m1 <= n)%nat /\ nsreachable m1 s /\ is_odd (porder m1)) /\ (forall s, valid_state s -> tc2i3 (encode_state s) s2 = true -> exists m1, (m1 <= n)%nat /\ nsreachable m1 s /\ porder m1 <> 1%positive) | _ => True end.
proof: Proof. generalize (iter2_equiv n) (iter2s_final n) (iter2s_valid n). case (iter2s n); case (iter2 n). intros (s1, s2) s3; case s3; auto. intros (l1, l2) l3; case l3; auto. intros (H1, (H2, _)); simpl in H1, H2. intros (H3, (H4, H5)) ((Hg1, Hg2),_); simpl in Hg1, Hg2. split; [idtac | split]. intros s Hs; case (H3 _ Hs); intros Hs1. assert (F1: In (rev3 (encode_state s)) (map (fun x : state => rev3 (encode_state x)) l1)). now rewrite in_map_iff; exists s; auto. rewrite <- (H1 (rev3 (encode_state s))) in F1. case (make_listtc2it3 _ _ _ F1); auto. rewrite rev3_involutive; auto. now intros (HH1, HH2); auto. assert (F1: In (rev3 (encode_state s)) (map (fun x : state => rev3 (encode_state x)) l2)). now rewrite in_map_iff; exists s; auto. rewrite <- (H2 (rev3 (encode_state s))) in F1. case (make_listtc2it3 _ _ _ F1); auto. rewrite rev3_involutive; auto. now intros (HH1, HH2); auto. intros s Hg Hs. assert (F1:= encode_valid _ Hg). rewrite <- (rev3_involutive (encode_state s)) in Hs, F1. generalize (make_listtc2ir3 _ _ nil F1 Hs). rewrite (H1 (rev3 (encode_state s))), in_map_iff. intros (s', (Hs', Hs1')). assert (s' = s); subst; auto. rewrite <- (encode_decode_state s'); auto. now rewrite Hs', encode_decode_state; auto. intros s Hg Hs. assert (F1:= encode_valid _ Hg). rewrite <- (rev3_involutive (encode_state s)) in Hs, F1. generalize (make_listtc2ir3 _ _ nil F1 Hs). rewrite (H2 (rev3 (encode_state s))), in_map_iff. intros (s', (Hs', Hs1')). assert (s' = s); subst; auto. rewrite <- (encode_decode_state s'); auto. now rewrite Hs', encode_decode_state; auto. intros s l (H1, (H2, H3)) _ ((Hg1, Hg2), _); simpl in H1, H2, H3, Hg1, Hg2. generalize (H3 (rev3 (encode_state s))). simpl tc2it; rewrite in_map_iff; intros [_ HH]. case HH; exists s; simpl; auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max