proposition: Lemma fold_next2_equiv p ss1 ss2 ss ll1 ll2 ll : valid_triple (ss1, ss2) -> (forall s, In s ss -> valid_state s) -> (forall s1, In s1 ss -> In s1 (fst ss1) \/ In s1 (snd ss1)) -> tstates_equiv (ss1, ss2) (ll1, ll2) -> states_equiv ss ll -> tstates_equiv (fold_left (next2s p) ss2 (ss1,ss)) (tc2it _ (next2p p) (ll1,ll) ll2).
proof: Proof. intros ((He1, He2), He3) He4 H1 (H2, (H3, H4)) H5. simpl in He1, He2, He3, H2, H3, H4. rewrite make_listtc2fold. unfold tstates_equiv; unfold states_equiv in H4. generalize ss1 ss2 ss ll1 ll He1 He2 He3 He4 H1 H2 H3 H4 H5. elim (tc2it _ make_list nil ll2); clear ss1 ss2 ss ll1 ll2 ll He1 He2 He3 He4 H1 H2 H3 H4 H5. intros ss1 ss2 ss ll1 ll He1 He2 He3 H4 H1 H2 H3; case ss2; auto. simpl; auto. intros s l HH; case (HH (rev3 (encode_state s))); intros _ HH1. now case HH1; simpl; auto with datatypes. intros. assert (F1: lequiv (map decode3 (a :: l)) ss2). intros s. split; intros H6. rewrite in_map_iff in H6; case H6; clear H6. intros l1 (Hl1, Hl2); subst. rewrite H4, in_map_iff in Hl2. case Hl2; intros s (Hs1, Hs2); subst. now rewrite encode_decode_state; auto. rewrite <- (encode_decode_state s); auto. apply (in_map decode3). rewrite H4. now apply (in_map (fun x => (rev3 (encode_state x)))); auto. rewrite fold_left_cons. case_eq (next2 p (ll1, ll) a); intros ll2 ll3 Hll2. case_eq (next2s p (ss1, ss) (decode3 a)); intros ss3 ss4 Hss3. assert (Fga: valid_state (decode3 a)). assert (F3: In a (a :: l)); auto with datatypes. rewrite H4, in_map_iff in F3; case F3; intros s (Hs1, Hs2); subst a. now rewrite encode_decode_state; auto. generalize (next2_equiv p (ss1, ss) (decode3 a) (ll1, ll) a); auto. rewrite Hss3; rewrite Hll2; intros HH; case HH; auto; clear HH; try (split; auto; fail). unfold state_equiv. assert (F3: In a (a :: l)); auto with datatypes. rewrite H4, in_map_iff in F3; case F3; intros s (Hs1, Hs2); subst a. now rewrite encode_decode_state; auto. simpl; intros Heq1 (Heq2, Heq3). case (H ss3 (map decode3 l) ss4 ll2 ll3); auto. - generalize (next2s_valid p (ss1, ss) (decode3 a)); auto. rewrite Hss3; intros HH; case HH; auto; clear HH. now split; auto. intros HH; case HH; auto. - generalize (next2s_valid p (ss1, ss) (decode3 a)); auto. rewrite Hss3; intros HH; case HH; auto; clear HH. now split; auto. intros HH; case HH; auto. - intros s Hs. rewrite in_map_iff in Hs; case Hs; intros l1 (Hl1, Hl2); subst. assert (F3: In l1 (a :: l)); auto with datatypes. rewrite H4, in_map_iff in F3. case F3; intros s (Hs1, Hs2); subst. rewrite encode_decode_state; auto. - generalize (next2s_valid p (ss1, ss) (decode3 a)); auto. rewrite Hss3; intros HH; case HH; auto; clear HH. now split; auto. - generalize (next2s_incl p (ss1,ss) (decode3 a)); rewrite Hss3; auto. - intros s; rewrite in_map_iff; split. intros Hs. assert (F2: In s (a :: l)); auto with datatypes. rewrite H4, in_map_iff in F2. case F2; intros s1 (Hs1, Hs2); subst. exists s1; split; auto. rewrite in_map_iff. exists (rev3 (encode_state s1)); split; auto. now rewrite <- encode_decode_state; auto. intros (s1, (Hs1, Hs2)); subst. rewrite in_map_iff in Hs2. case Hs2; intros l1 (Hl1, Hl2); subst. assert (F2: In l1 (a :: l)); auto with datatypes. rewrite H4, in_map_iff in F2. case F2; intros s1 (Hs3, Hs4); subst. rewrite (encode_decode_state s1); auto. - intros F2 (F3, F4). case (fold_next2s_equiv p (ss1, (map decode3 (a :: l))) (ss1, ss2) ss ss); simpl; auto. + split; simpl; auto. now intros s; split; auto. split; auto. intros s; split; auto. + intros s; split; auto. + unfold BasicRubik.states in Hss3 |- *; rewrite Hss3. intros H6 (H7, H8). split. generalize F2; rewrite <- Hll2; case a; clear F2. intros (lc,lo) p1 F2. now apply states_equiv_equiv with (1 := F2); auto. split. generalize F3; rewrite <- Hll2; case a; clear F3. intros (lc,lo) p1 F3. now apply states_equiv_equiv with (1 := F3); auto. generalize F4; rewrite <- Hll2; case a; clear F4. intros (lc,lo) p1 F4. apply states_equiv_equiv with (1 := F4); auto. Qed.
imports: PrimInt63 Cyclic63 List BasicRubik Max