Untitled

Goal (∀ n, ∀ edges, ∀ start, ∀ F, ∀ A: NFA n "()" edges start F, ~ (Lnfa A = {s | valid_paren s}));
Proof;
intros;
add_hyp (∃ x y z: list char, repeat n '(' = x + y + z ∧ 0 < |y| ∧ |x| + |z| ≤ n ∧ ∀ i: ℤ, 0 ≤ i → run_nfa A start (x + rep y i + z) = run_nfa A start (repeat n '('));
apply pumping_lemma;
replace #1 (|repeat n '('|) with (n);
apply repeat_len;
Switch 1;
auto_list;
Switch 1;
apply IsWord_fold;
apply included_fold;
intros;
replace #1 (member_set (repeat n '(')) with ({'('}) in H0;
apply member_set_repeat;
Switch 1;
replace #1 (member_set "()") with ({'('} ∪ member_set ")");
apply member_set_cons_union;
auto_set;
Switch 2;
destruct H0 with (ex_ind ? ?) to (x x_property);
destruct x_property with (ex_ind ? ?) to (y y_property);
destruct y_property with (ex_ind ? ?) to (z z_property);
add_hyp ((x + y + y + z) + repeat n ')' ∈ Lnfa A);
apply Lnfa_fold;
apply and_intro;
replace #1 (run_nfa A start (x + y + y + z + repeat n ')')) with (run_nfa A start (x + y + z + repeat n ')'));
replace #1 (run_nfa A start (x + y + y + z + repeat n ')')) with (run_nfa A (run_nfa A start (x + y + y + z) ) (repeat n ')'));
apply run_nfa_append;
replace #1 (run_nfa A start (x + y + y + z)) with (run_nfa A start (x + y + z));
destruct z_property with (and_ind ? ?) to (z_property_l z_property_r) ;
destruct z_property_r with (and_ind ? ?) to (z_property_r_l z_property_r_r) ;
destruct z_property_r_r with (and_ind ? ?) to (z_property_r_r_l z_property_r_r_r) ;
add_hyp z_property_r_r_r_ex := (z_property_r_r_r (2));
Seq (add_hyp (⁨0 ≤ 2⁩)) (remove_hyp z_property_r_r_r_ex) (Switch 1) (add_hyp z_property_r_r_r_ex_o := (z_property_r_r_r_ex H0)) (remove_hyp H0) (remove_hyp z_property_r_r_r_ex) ;
replace #1 (rep y 2) with (y + y) in z_property_r_r_r_ex_o;
Switch 1;
replace #1 ((x + (y + y) + z)) with ((x + y + y + z)) in z_property_r_r_r_ex_o;
auto_list;
apply eq_sym in z_property_l ;
rewrite z_property_l ;
assumption;
Switch 1;
lia;
Switch 1;
apply eq_sym ;
apply run_nfa_append;
Switch 1;
destruct z_property with (and_ind ? ?) to (z_property_l z_property_r) ;
apply eq_sym in z_property_l ;
rewrite z_property_l ;
add_hyp ((repeat n '(' + repeat n ')') ∈ Lnfa A);
rewrite H ;
apply set_from_func_fold ;
Switch 1;
apply Lnfa_unfold in H0;
assumption;
Switch 3;
revert H0;
rewrite H ;
intros;
apply set_from_func_unfold in H0 ;