Untitled

Goal (star {"aa", "aaa"} =  words "a" ∖ {"a"});
Proof;
apply set_equality;
apply included_fold;
intros;
apply setminus_unfold in H;
destruct H with (and_ind ? ?) to (H_l H_r);
apply in_words_unfold in H_l;
add_hyp (even (|a|) ∨ odd (|a|));
apply even_or_odd;
destruct H with (or_ind ? ?);
apply odd_unfold in H;
destruct H with (ex_ind ? ?) to (k k_property);
add_hyp (a = rep "aa" (k - 1) + "aaa");
apply (⁨nth_eq ?0 '*' ?4 ?6 ?8 ?10⁩);
intros;
apply IsWord_unfold in H_l;
apply included_unfold in H_l;
add_hyp H_l_ex := (H_l (nth '*' a i));
Seq (add_hyp (⁨nth '*' a i ∈ member_set a⁩)) (remove_hyp H_l_ex) (Switch 1) (add_hyp H_l_ex_o := (H_l_ex H0)) (remove_hyp H0) (remove_hyp H_l_ex);
replace #1 (member_set "a") with ({'a'}) in H_l_ex_o;
apply member_set_singleton;
apply singleton_unfold in H_l_ex_o;
add_hyp (i < |rep "aa" (k - 1)| ∨ i ≥ |rep "aa" (k - 1)|);
lia;
destruct H0 with (or_ind ? ?);
replace #1 (nth '*' (rep "aa" (k - 1) + "aaa") i) with (nth '*' ("aaa") (i - |rep "aa" (k - 1)|));
apply nth_append_r;
add_hyp (|a| = |rep "aa" (k - 1) + "aaa"|);
replace #1 (|rep "aa" (k - 1) + "aaa"|) with (|rep "aa" (k - 1)| + 3);
lia;
replace #1 (|rep "aa" (k - 1)|) with ( (k - 1) * |"aa"|);
apply rep_len;
z3;
lia;
lia;
add_hyp (i < |rep "aa" (k - 1)| + 3);
add_hyp (|a| = |rep "aa" (k - 1) + "aaa"|);
replace #1 (|rep "aa" (k - 1) + "aaa"|) with (|rep "aa" (k - 1)| + 3);
lia;
replace #1 (|rep "aa" (k - 1)|) with ( (k - 1) * |"aa"|);
apply rep_len;
z3;
lia;
lia;
z3;
replace #1 (nth '*' (rep "aa" (k - 1) + "aaa") i) with (nth '*' (rep "aa" (k - 1)) i);
z3;
replace #1 (nth '*' (rep "aa" (k - 1)) i) with (nth '*' ( "aa" ) (i mod 2));
replace #1 (2) with (|"aa"|);
lia;
apply rep_nth;
replace #1 (|rep "aa" (k - 1)|) with ( (k - 1) * |"aa"|) in H0;
apply rep_len;
z3;
assumption;
apply NNPP;
intros;
add_hyp (|a| = 3);
z3;
replace #1 (rep "aa" (k - 1)) with ("") in H0;
replace #1 ((k - 1)) with (0);
lia;
apply rep_0;
lia;
z3;
apply inlist_member_set;
z3;
replace #1 (|rep "aa" (k - 1) + "aaa"|) with (|rep "aa" (k - 1) | + 3);
lia;
replace #1 (|rep "aa" (k - 1)|) with ((k - 1) * |"aa"|);
apply rep_len;
apply NNPP;
intros;
add_hyp (k = 0);
lia;
apply IsWord_unfold in H_l;
apply included_unfold in H_l;
add_hyp H_l_ex := (H_l (head '*' a));
Seq (add_hyp (⁨head '*' a ∈ member_set a⁩)) (remove_hyp H_l_ex) (Switch 1) (add_hyp H_l_ex_o := (H_l_ex H1)) (remove_hyp H1) (remove_hyp H_l_ex);
replace #1 (member_set "a") with ({'a'}) in H_l_ex_o;
apply member_set_singleton;
z3;
apply inlist_member_set;
z3;
lia;
rewrite H;
apply star_append;
apply (⁨star_fold ?0 ?2 1 ?6 ?8⁩);
replace #1 (lpow {"aa", "aaa"} 1) with ( {"aa", "aaa"} );
apply lpow_1;
auto_set;
lia;
apply (⁨star_fold ?0 ?2 (k - 1) ?6 ?8⁩);
apply rep_in_lpow;
z3;
auto_set;
z3;
add_hyp (|a| = 0 ∨ |a| > 0);
lia;
destruct H0 with (or_ind ? ?);
apply even_unfold in H;
destruct H with (ex_ind ? ?) to (k k_property);
add_hyp (a = rep "aa" k);
apply (⁨nth_eq ?0 '*' ?4 ?6 ?8 ?10⁩);
intros;
replace #1 (nth '*' (rep "aa" k) i) with ('a');
replace #1 (nth '*' (rep "aa" k) i) with (nth '*' ("aa") (i mod |"aa"|));
apply rep_nth;
lia;
lia;
z3;
apply IsWord_unfold in H_l;
apply included_unfold in H_l;
add_hyp H_l_ex := (H_l (nth '*' a i));
Seq (add_hyp (⁨nth '*' a i ∈ member_set a⁩)) (remove_hyp H_l_ex) (Switch 1) (add_hyp H_l_ex_o := (H_l_ex H1)) (remove_hyp H1) (remove_hyp H_l_ex);
replace #1 (member_set "a") with ({'a'}) in H_l_ex_o;
apply member_set_singleton;
auto_set;
apply inlist_member_set;
apply in_nth;
assumption;
replace #1 (|rep "aa" k|) with (k * |"aa" |);
apply rep_len;
lia;
lia;
apply (⁨star_fold ?0 ?2 k ?6 ?8⁩);
rewrite H;
apply rep_in_lpow;
lia;
auto_set;
lia;
apply even_unfold in H;
destruct H with (ex_ind ? ?) to (k k_property);
add_hyp (a = rep "aa" k);
apply (⁨nth_eq ?0 '*' ?4 ?6 ?8 ?10⁩);
intros;
replace #1 (nth '*' (rep "aa" k) i) with ('a');
replace #1 (nth '*' (rep "aa" k) i) with (nth '*' ("aa") (i mod |"aa"|));
apply rep_nth;
lia;
lia;
z3;
apply IsWord_unfold in H_l;
apply included_unfold in H_l;
add_hyp H_l_ex := (H_l (nth '*' a i));
Seq (add_hyp (⁨nth '*' a i ∈ member_set a⁩)) (remove_hyp H_l_ex) (Switch 1) (add_hyp H_l_ex_o := (H_l_ex H1)) (remove_hyp H1) (remove_hyp H_l_ex);
replace #1 (member_set "a") with ({'a'}) in H_l_ex_o;
apply member_set_singleton;
auto_set;
apply inlist_member_set;
apply in_nth;
assumption;
replace #1 (|rep "aa" k|) with (k * |"aa" |);
apply rep_len;
lia;
lia;
apply (⁨star_fold ?0 ?2 k ?6 ?8⁩);
rewrite H;
apply rep_in_lpow;
lia;
auto_set;
lia;
add_hyp (star {"aa", "aaa"} ⊆ words "a");
apply star_incl_sigma;
Switch 1;
apply included_fold ;
intros;
apply setminus_fold ;
apply and_intro ;
intros;
apply star_unfold in H0 ;
destruct H0 with (ex_ind ? ?) to (n n_property);
destruct n_property with (and_ind ? ?) to (n_property_l n_property_r) ;
destruct n_property_l with (or_ind ? ?) ;
add_hyp (|a| = 0);
replace #1 (lpow {"aa", "aaa"} n) with ({""}) in n_property_r;
apply eq_sym in n_property_l ;
rewrite n_property_l ;
apply lpow_0;
z3;
z3;
replace #1 (lpow {"aa", "aaa"} n) with ({"aa", "aaa"} * lpow {"aa", "aaa"} (n - 1)) in n_property_r;
replace #1 (n) with ((n - 1) + 1);
lia;
apply lpow_unfold;
lia;
apply in_Lmult_unfold in n_property_r ;
destruct n_property_r with (ex_ind ? ?) to (x x_property);
destruct x_property with (ex_ind ? ?) to (y y_property);
z3;
auto_set;