BA003D

cf_convergent_euclidean_matrix_step_alignment

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The actual G071 history and actual matrix prefix consume the same first quotient and tagged tail; both predecessor computations and all recurrence equations are derived, not assumed.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded first-order arithmetic statement

forall a b s h e L H E k u U v V. (exists cf_gcd_alignment_old. ((((exists ff_h_cf_alignment_old_initial_state. ff_h_cf_alignment_old_initial_state + S (((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_alignment_old_initial_state. h = ff_q_cf_alignment_old_initial_state * S ((S (0)) * e) + (((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_old) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_alignment_old_terminal_state. ff_h_cf_alignment_old_terminal_state + S (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))) = S ((S (L)) * e)) /\ exists ff_q_cf_alignment_old_terminal_state. h = ff_q_cf_alignment_old_terminal_state * S ((S (L)) * e) + (((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) * S ((a) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s)))) + ((((b) + (s)) * S ((b) + (s)) + ((s) + (s))) + (((b) + (s)) * S ((b) + (s)) + ((s) + (s))))))) /\ forall cf_index_alignment_old. (exists ff_lt_cf_alignment_old_index. ff_lt_cf_alignment_old_index + S cf_index_alignment_old = L) -> exists cf_old_a_alignment_old cf_old_b_alignment_old cf_tail_alignment_old cf_new_a_alignment_old cf_new_b_alignment_old cf_head_alignment_old cf_quotient_alignment_old. ((((exists ff_h_cf_alignment_old_previous_state. ff_h_cf_alignment_old_previous_state + S (((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) * S ((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) + ((((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))))) = S ((S (cf_index_alignment_old)) * e)) /\ exists ff_q_cf_alignment_old_previous_state. h = ff_q_cf_alignment_old_previous_state * S ((S (cf_index_alignment_old)) * e) + (((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) * S ((cf_old_a_alignment_old) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old)))) + ((((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))) + (((cf_old_b_alignment_old) + (cf_tail_alignment_old)) * S ((cf_old_b_alignment_old) + (cf_tail_alignment_old)) + ((cf_tail_alignment_old) + (cf_tail_alignment_old))))))) /\ ((((exists ff_h_cf_alignment_old_following_state. ff_h_cf_alignment_old_following_state + S (((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) * S ((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) + ((((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))))) = S ((S (S cf_index_alignment_old)) * e)) /\ exists ff_q_cf_alignment_old_following_state. h = ff_q_cf_alignment_old_following_state * S ((S (S cf_index_alignment_old)) * e) + (((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) * S ((cf_new_a_alignment_old) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old)))) + ((((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))) + (((cf_new_b_alignment_old) + (cf_head_alignment_old)) * S ((cf_new_b_alignment_old) + (cf_head_alignment_old)) + ((cf_head_alignment_old) + (cf_head_alignment_old))))))) /\ (cf_new_b_alignment_old = cf_old_a_alignment_old /\ (cf_new_a_alignment_old = cf_new_b_alignment_old * cf_quotient_alignment_old + cf_old_b_alignment_old /\ ((exists ff_lt_cf_alignment_old_remainder. ff_lt_cf_alignment_old_remainder + S cf_old_b_alignment_old = cf_new_b_alignment_old) /\ (cf_head_alignment_old = S ((cf_quotient_alignment_old + cf_tail_alignment_old) * S (cf_quotient_alignment_old + cf_tail_alignment_old) + (cf_tail_alignment_old + cf_tail_alignment_old))))))))))) -> (exists cfc_tail_alignment_new. ((exists cfc_state_alignment_newinitial. ((exists cfc_left_alignment_newinitialcode cfc_right_alignment_newinitialcode cfc_matrix_alignment_newinitialcode. ((cfc_left_alignment_newinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_alignment_newinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_alignment_newinitialcode = ((cfc_left_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode)) * S ((cfc_left_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode)) + ((cfc_right_alignment_newinitialcode) + (cfc_right_alignment_newinitialcode))) /\ ((cfc_state_alignment_newinitial) = ((cfc_tail_alignment_new) + (cfc_matrix_alignment_newinitialcode)) * S ((cfc_tail_alignment_new) + (cfc_matrix_alignment_newinitialcode)) + ((cfc_matrix_alignment_newinitialcode) + (cfc_matrix_alignment_newinitialcode))))))) /\ (((exists ff_h_alignment_newinitialentry. ff_h_alignment_newinitialentry + S (cfc_state_alignment_newinitial) = S ((S (0)) * E)) /\ exists ff_q_alignment_newinitialentry. H = ff_q_alignment_newinitialentry * S ((S (0)) * E) + (cfc_state_alignment_newinitial))))) /\ ((exists cfc_state_alignment_newterminal. ((exists cfc_left_alignment_newterminalcode cfc_right_alignment_newterminalcode cfc_matrix_alignment_newterminalcode. ((cfc_left_alignment_newterminalcode = ((u) + (U)) * S ((u) + (U)) + ((U) + (U))) /\ ((cfc_right_alignment_newterminalcode = ((v) + (V)) * S ((v) + (V)) + ((V) + (V))) /\ ((cfc_matrix_alignment_newterminalcode = ((cfc_left_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode)) * S ((cfc_left_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode)) + ((cfc_right_alignment_newterminalcode) + (cfc_right_alignment_newterminalcode))) /\ ((cfc_state_alignment_newterminal) = ((s) + (cfc_matrix_alignment_newterminalcode)) * S ((s) + (cfc_matrix_alignment_newterminalcode)) + ((cfc_matrix_alignment_newterminalcode) + (cfc_matrix_alignment_newterminalcode))))))) /\ (((exists ff_h_alignment_newterminalentry. ff_h_alignment_newterminalentry + S (cfc_state_alignment_newterminal) = S ((S (S k)) * E)) /\ exists ff_q_alignment_newterminalentry. H = ff_q_alignment_newterminalentry * S ((S (S k)) * E) + (cfc_state_alignment_newterminal))))) /\ (forall cfc_index_alignment_new. (exists cfba_gap_alignment_newbound. cfba_gap_alignment_newbound + S (cfc_index_alignment_new) = (S k)) -> exists cfc_old_alignment_new cfc_a_alignment_new cfc_b_alignment_new cfc_c_alignment_new cfc_d_alignment_new cfc_new_alignment_new cfc_quotient_alignment_new. ((exists cfc_state_alignment_newprevious. ((exists cfc_left_alignment_newpreviouscode cfc_right_alignment_newpreviouscode cfc_matrix_alignment_newpreviouscode. ((cfc_left_alignment_newpreviouscode = ((cfc_a_alignment_new) + (cfc_b_alignment_new)) * S ((cfc_a_alignment_new) + (cfc_b_alignment_new)) + ((cfc_b_alignment_new) + (cfc_b_alignment_new))) /\ ((cfc_right_alignment_newpreviouscode = ((cfc_c_alignment_new) + (cfc_d_alignment_new)) * S ((cfc_c_alignment_new) + (cfc_d_alignment_new)) + ((cfc_d_alignment_new) + (cfc_d_alignment_new))) /\ ((cfc_matrix_alignment_newpreviouscode = ((cfc_left_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode)) * S ((cfc_left_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode)) + ((cfc_right_alignment_newpreviouscode) + (cfc_right_alignment_newpreviouscode))) /\ ((cfc_state_alignment_newprevious) = ((cfc_old_alignment_new) + (cfc_matrix_alignment_newpreviouscode)) * S ((cfc_old_alignment_new) + (cfc_matrix_alignment_newpreviouscode)) + ((cfc_matrix_alignment_newpreviouscode) + (cfc_matrix_alignment_newpreviouscode))))))) /\ (((exists ff_h_alignment_newpreviousentry. ff_h_alignment_newpreviousentry + S (cfc_state_alignment_newprevious) = S ((S (cfc_index_alignment_new)) * E)) /\ exists ff_q_alignment_newpreviousentry. H = ff_q_alignment_newpreviousentry * S ((S (cfc_index_alignment_new)) * E) + (cfc_state_alignment_newprevious))))) /\ ((exists cfc_state_alignment_newfollowing. ((exists cfc_left_alignment_newfollowingcode cfc_right_alignment_newfollowingcode cfc_matrix_alignment_newfollowingcode. ((cfc_left_alignment_newfollowingcode = (((cfc_quotient_alignment_new * cfc_a_alignment_new + cfc_c_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new))) * S (((cfc_quotient_alignment_new * cfc_a_alignment_new + cfc_c_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new))) + (((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new)) + ((cfc_quotient_alignment_new * cfc_b_alignment_new + cfc_d_alignment_new)))) /\ ((cfc_right_alignment_newfollowingcode = ((cfc_a_alignment_new) + (cfc_b_alignment_new)) * S ((cfc_a_alignment_new) + (cfc_b_alignment_new)) + ((cfc_b_alignment_new) + (cfc_b_alignment_new))) /\ ((cfc_matrix_alignment_newfollowingcode = ((cfc_left_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode)) * S ((cfc_left_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode)) + ((cfc_right_alignment_newfollowingcode) + (cfc_right_alignment_newfollowingcode))) /\ ((cfc_state_alignment_newfollowing) = ((cfc_new_alignment_new) + (cfc_matrix_alignment_newfollowingcode)) * S ((cfc_new_alignment_new) + (cfc_matrix_alignment_newfollowingcode)) + ((cfc_matrix_alignment_newfollowingcode) + (cfc_matrix_alignment_newfollowingcode))))))) /\ (((exists ff_h_alignment_newfollowingentry. ff_h_alignment_newfollowingentry + S (cfc_state_alignment_newfollowing) = S ((S (S cfc_index_alignment_new)) * E)) /\ exists ff_q_alignment_newfollowingentry. H = ff_q_alignment_newfollowingentry * S ((S (S cfc_index_alignment_new)) * E) + (cfc_state_alignment_newfollowing))))) /\ (cfc_new_alignment_new = S ((cfc_quotient_alignment_new + cfc_old_alignment_new) * S (cfc_quotient_alignment_new + cfc_old_alignment_new) + (cfc_old_alignment_new + cfc_old_alignment_new))))))))) -> (exists cfc_r_alignment_result cfc_tail_alignment_result cfc_length_alignment_result cfc_q_alignment_result cfc_p_alignment_result cfc_P_alignment_result cfc_n_alignment_result cfc_N_alignment_result. (((L) = S cfc_length_alignment_result) /\ (((a) = (b) * cfc_q_alignment_result + cfc_r_alignment_result) /\ ((exists cfba_gap_alignment_resultbound. cfba_gap_alignment_resultbound + S (cfc_r_alignment_result) = (b)) /\ ((exists cf_gcd_alignment_resulteuclidean. ((((exists ff_h_cf_alignment_resulteuclidean_initial_state. ff_h_cf_alignment_resulteuclidean_initial_state + S (((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_initial_state. h = ff_q_cf_alignment_resulteuclidean_initial_state * S ((S (0)) * e) + (((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_resulteuclidean) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_alignment_resulteuclidean_terminal_state. ff_h_cf_alignment_resulteuclidean_terminal_state + S (((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) * S ((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) + ((((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))))) = S ((S (cfc_length_alignment_result)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_terminal_state. h = ff_q_cf_alignment_resulteuclidean_terminal_state * S ((S (cfc_length_alignment_result)) * e) + (((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) * S ((b) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result)))) + ((((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))) + (((cfc_r_alignment_result) + (cfc_tail_alignment_result)) * S ((cfc_r_alignment_result) + (cfc_tail_alignment_result)) + ((cfc_tail_alignment_result) + (cfc_tail_alignment_result))))))) /\ forall cf_index_alignment_resulteuclidean. (exists ff_lt_cf_alignment_resulteuclidean_index. ff_lt_cf_alignment_resulteuclidean_index + S cf_index_alignment_resulteuclidean = cfc_length_alignment_result) -> exists cf_old_a_alignment_resulteuclidean cf_old_b_alignment_resulteuclidean cf_tail_alignment_resulteuclidean cf_new_a_alignment_resulteuclidean cf_new_b_alignment_resulteuclidean cf_head_alignment_resulteuclidean cf_quotient_alignment_resulteuclidean. ((((exists ff_h_cf_alignment_resulteuclidean_previous_state. ff_h_cf_alignment_resulteuclidean_previous_state + S (((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) * S ((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) + ((((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))))) = S ((S (cf_index_alignment_resulteuclidean)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_previous_state. h = ff_q_cf_alignment_resulteuclidean_previous_state * S ((S (cf_index_alignment_resulteuclidean)) * e) + (((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) * S ((cf_old_a_alignment_resulteuclidean) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)))) + ((((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))) + (((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) * S ((cf_old_b_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean)) + ((cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean))))))) /\ ((((exists ff_h_cf_alignment_resulteuclidean_following_state. ff_h_cf_alignment_resulteuclidean_following_state + S (((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) * S ((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) + ((((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))))) = S ((S (S cf_index_alignment_resulteuclidean)) * e)) /\ exists ff_q_cf_alignment_resulteuclidean_following_state. h = ff_q_cf_alignment_resulteuclidean_following_state * S ((S (S cf_index_alignment_resulteuclidean)) * e) + (((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) * S ((cf_new_a_alignment_resulteuclidean) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)))) + ((((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))) + (((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) * S ((cf_new_b_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean)) + ((cf_head_alignment_resulteuclidean) + (cf_head_alignment_resulteuclidean))))))) /\ (cf_new_b_alignment_resulteuclidean = cf_old_a_alignment_resulteuclidean /\ (cf_new_a_alignment_resulteuclidean = cf_new_b_alignment_resulteuclidean * cf_quotient_alignment_resulteuclidean + cf_old_b_alignment_resulteuclidean /\ ((exists ff_lt_cf_alignment_resulteuclidean_remainder. ff_lt_cf_alignment_resulteuclidean_remainder + S cf_old_b_alignment_resulteuclidean = cf_new_b_alignment_resulteuclidean) /\ (cf_head_alignment_resulteuclidean = S ((cf_quotient_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean) * S (cf_quotient_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean) + (cf_tail_alignment_resulteuclidean + cf_tail_alignment_resulteuclidean))))))))))) /\ ((exists cfc_tail_alignment_resultmatrix. ((exists cfc_state_alignment_resultmatrixinitial. ((exists cfc_left_alignment_resultmatrixinitialcode cfc_right_alignment_resultmatrixinitialcode cfc_matrix_alignment_resultmatrixinitialcode. ((cfc_left_alignment_resultmatrixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_alignment_resultmatrixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_alignment_resultmatrixinitialcode = ((cfc_left_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode)) * S ((cfc_left_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode)) + ((cfc_right_alignment_resultmatrixinitialcode) + (cfc_right_alignment_resultmatrixinitialcode))) /\ ((cfc_state_alignment_resultmatrixinitial) = ((cfc_tail_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixinitialcode)) * S ((cfc_tail_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixinitialcode)) + ((cfc_matrix_alignment_resultmatrixinitialcode) + (cfc_matrix_alignment_resultmatrixinitialcode))))))) /\ (((exists ff_h_alignment_resultmatrixinitialentry. ff_h_alignment_resultmatrixinitialentry + S (cfc_state_alignment_resultmatrixinitial) = S ((S (0)) * E)) /\ exists ff_q_alignment_resultmatrixinitialentry. H = ff_q_alignment_resultmatrixinitialentry * S ((S (0)) * E) + (cfc_state_alignment_resultmatrixinitial))))) /\ ((exists cfc_state_alignment_resultmatrixterminal. ((exists cfc_left_alignment_resultmatrixterminalcode cfc_right_alignment_resultmatrixterminalcode cfc_matrix_alignment_resultmatrixterminalcode. ((cfc_left_alignment_resultmatrixterminalcode = ((cfc_p_alignment_result) + (cfc_P_alignment_result)) * S ((cfc_p_alignment_result) + (cfc_P_alignment_result)) + ((cfc_P_alignment_result) + (cfc_P_alignment_result))) /\ ((cfc_right_alignment_resultmatrixterminalcode = ((cfc_n_alignment_result) + (cfc_N_alignment_result)) * S ((cfc_n_alignment_result) + (cfc_N_alignment_result)) + ((cfc_N_alignment_result) + (cfc_N_alignment_result))) /\ ((cfc_matrix_alignment_resultmatrixterminalcode = ((cfc_left_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode)) * S ((cfc_left_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode)) + ((cfc_right_alignment_resultmatrixterminalcode) + (cfc_right_alignment_resultmatrixterminalcode))) /\ ((cfc_state_alignment_resultmatrixterminal) = ((cfc_tail_alignment_result) + (cfc_matrix_alignment_resultmatrixterminalcode)) * S ((cfc_tail_alignment_result) + (cfc_matrix_alignment_resultmatrixterminalcode)) + ((cfc_matrix_alignment_resultmatrixterminalcode) + (cfc_matrix_alignment_resultmatrixterminalcode))))))) /\ (((exists ff_h_alignment_resultmatrixterminalentry. ff_h_alignment_resultmatrixterminalentry + S (cfc_state_alignment_resultmatrixterminal) = S ((S (k)) * E)) /\ exists ff_q_alignment_resultmatrixterminalentry. H = ff_q_alignment_resultmatrixterminalentry * S ((S (k)) * E) + (cfc_state_alignment_resultmatrixterminal))))) /\ (forall cfc_index_alignment_resultmatrix. (exists cfba_gap_alignment_resultmatrixbound. cfba_gap_alignment_resultmatrixbound + S (cfc_index_alignment_resultmatrix) = (k)) -> exists cfc_old_alignment_resultmatrix cfc_a_alignment_resultmatrix cfc_b_alignment_resultmatrix cfc_c_alignment_resultmatrix cfc_d_alignment_resultmatrix cfc_new_alignment_resultmatrix cfc_quotient_alignment_resultmatrix. ((exists cfc_state_alignment_resultmatrixprevious. ((exists cfc_left_alignment_resultmatrixpreviouscode cfc_right_alignment_resultmatrixpreviouscode cfc_matrix_alignment_resultmatrixpreviouscode. ((cfc_left_alignment_resultmatrixpreviouscode = ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) * S ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) + ((cfc_b_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix))) /\ ((cfc_right_alignment_resultmatrixpreviouscode = ((cfc_c_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix)) * S ((cfc_c_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix)) + ((cfc_d_alignment_resultmatrix) + (cfc_d_alignment_resultmatrix))) /\ ((cfc_matrix_alignment_resultmatrixpreviouscode = ((cfc_left_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode)) * S ((cfc_left_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode)) + ((cfc_right_alignment_resultmatrixpreviouscode) + (cfc_right_alignment_resultmatrixpreviouscode))) /\ ((cfc_state_alignment_resultmatrixprevious) = ((cfc_old_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixpreviouscode)) * S ((cfc_old_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixpreviouscode)) + ((cfc_matrix_alignment_resultmatrixpreviouscode) + (cfc_matrix_alignment_resultmatrixpreviouscode))))))) /\ (((exists ff_h_alignment_resultmatrixpreviousentry. ff_h_alignment_resultmatrixpreviousentry + S (cfc_state_alignment_resultmatrixprevious) = S ((S (cfc_index_alignment_resultmatrix)) * E)) /\ exists ff_q_alignment_resultmatrixpreviousentry. H = ff_q_alignment_resultmatrixpreviousentry * S ((S (cfc_index_alignment_resultmatrix)) * E) + (cfc_state_alignment_resultmatrixprevious))))) /\ ((exists cfc_state_alignment_resultmatrixfollowing. ((exists cfc_left_alignment_resultmatrixfollowingcode cfc_right_alignment_resultmatrixfollowingcode cfc_matrix_alignment_resultmatrixfollowingcode. ((cfc_left_alignment_resultmatrixfollowingcode = (((cfc_quotient_alignment_resultmatrix * cfc_a_alignment_resultmatrix + cfc_c_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix))) * S (((cfc_quotient_alignment_resultmatrix * cfc_a_alignment_resultmatrix + cfc_c_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix))) + (((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix)) + ((cfc_quotient_alignment_resultmatrix * cfc_b_alignment_resultmatrix + cfc_d_alignment_resultmatrix)))) /\ ((cfc_right_alignment_resultmatrixfollowingcode = ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) * S ((cfc_a_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix)) + ((cfc_b_alignment_resultmatrix) + (cfc_b_alignment_resultmatrix))) /\ ((cfc_matrix_alignment_resultmatrixfollowingcode = ((cfc_left_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode)) * S ((cfc_left_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode)) + ((cfc_right_alignment_resultmatrixfollowingcode) + (cfc_right_alignment_resultmatrixfollowingcode))) /\ ((cfc_state_alignment_resultmatrixfollowing) = ((cfc_new_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixfollowingcode)) * S ((cfc_new_alignment_resultmatrix) + (cfc_matrix_alignment_resultmatrixfollowingcode)) + ((cfc_matrix_alignment_resultmatrixfollowingcode) + (cfc_matrix_alignment_resultmatrixfollowingcode))))))) /\ (((exists ff_h_alignment_resultmatrixfollowingentry. ff_h_alignment_resultmatrixfollowingentry + S (cfc_state_alignment_resultmatrixfollowing) = S ((S (S cfc_index_alignment_resultmatrix)) * E)) /\ exists ff_q_alignment_resultmatrixfollowingentry. H = ff_q_alignment_resultmatrixfollowingentry * S ((S (S cfc_index_alignment_resultmatrix)) * E) + (cfc_state_alignment_resultmatrixfollowing))))) /\ (cfc_new_alignment_resultmatrix = S ((cfc_quotient_alignment_resultmatrix + cfc_old_alignment_resultmatrix) * S (cfc_quotient_alignment_resultmatrix + cfc_old_alignment_resultmatrix) + (cfc_old_alignment_resultmatrix + cfc_old_alignment_resultmatrix))))))))) /\ (((u) = cfc_q_alignment_result * cfc_p_alignment_result + cfc_n_alignment_result) /\ (((U) = cfc_q_alignment_result * cfc_P_alignment_result + cfc_N_alignment_result) /\ (((v) = cfc_p_alignment_result) /\ ((V) = cfc_P_alignment_result))))))))))

Constructive proof overview

Generated structural guide

The actual G071 history and actual matrix prefix consume the same first quotient and tagged tail; both predecessor computations and all recurrence equations are derived, not assumed.

The unchanged tactic script uses 5 declared prerequisites and contains 116 exact native proof lines.

Alpha v34 checked-use · first admitted v29 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

BA0034 cf_convergent_matrix_nonempty_list BA002D cf_convergent_old_history_nonempty_head BA0033 cf_convergent_matrix_successor_elimination cell_functional Alpha theorem; checked-use authorized BA0035 cf_convergent_matrix_list_transport

Direct dependents

BA003E cf_convergent_actual_prefix_error_invariant BA0040 cf_convergent_actual_prefix_index_bound BA0047 cf_convergent_full_matrix_is_exact

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

116 script commands · 32 reading checkpoints · 4 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
cf convergent matrix nonempty listcf convergent old history nonempty headcf convergent matrix successor eliminationcf convergent matrix list transport

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro s
  4. L4
    intro h
  5. L5
    intro e
  6. L6
    intro L
  7. L7
    intro H
  8. L8
    intro E
  9. L9
    intro k
  10. L10
    intro u
02Fix variables and assumptionsL11–15

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro U
  2. L12
    intro v
  3. L13
    intro V
  4. L14
    intro hold
  5. L15
    intro hnew
03Establish hnL16–25

Establish this local claim before using it. It is not an additional assumption.

  1. L16
    have hn : ~(s = 0)
  2. L17
    intro hz
  3. L18
    specialize cf_convergent_matrix_nonempty_list (s)
  4. L19
    specialize cf_convergent_matrix_nonempty_list (H)
  5. L20
    specialize cf_convergent_matrix_nonempty_list (E)
  6. L21
    specialize cf_convergent_matrix_nonempty_list (k)
  7. L22
    specialize cf_convergent_matrix_nonempty_list (u)
  8. L23
    specialize cf_convergent_matrix_nonempty_list (U)
  9. L24
    specialize cf_convergent_matrix_nonempty_list (v)
  10. L25
    specialize cf_convergent_matrix_nonempty_list (V)
04Use earlier factsL26–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L26
    apply cf_convergent_matrix_nonempty_list
  2. L27
    exact hnew
  3. L28
    exact hz
05Establish hhL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent old history nonempty head.

  1. L29
    have hh : ∃ cfc_q_alignment_head. ∃ cfc_r_alignment_head. ∃ cfc_tail_alignment_head. ∃ cfc_length_alignment_head. L = S cfc_length_alignment_head ∧ (a = b · cfc_q_alignment_head + cfc_r_alignment_head ∧ (Lt(cfc_r_alignment_head,b) ∧ (ListCell(s,cfc_q_alignment_head,cfc_tail_alignment_head) ∧ ContinuedFractionTrace(b,cfc_r_alignment_head,cfc_tail_alignment_head,h,e,cfc_length_alignment_head))))Definitions: ListCellContinuedFractionTraceLt
  2. L30
    specialize cf_convergent_old_history_nonempty_head (a)
  3. L31
    specialize cf_convergent_old_history_nonempty_head (b)
  4. L32
    specialize cf_convergent_old_history_nonempty_head (s)
  5. L33
    specialize cf_convergent_old_history_nonempty_head (h)
  6. L34
    specialize cf_convergent_old_history_nonempty_head (e)
  7. L35
    specialize cf_convergent_old_history_nonempty_head (L)
  8. L36
    apply cf_convergent_old_history_nonempty_head
  9. L37
    exact hold
  10. L38
    exact hn
06Separate the logical casesL39–46

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L39
    cases hh
  2. L40
    cases hh_witness
  3. L41
    cases hh_witness_witness
  4. L42
    cases hh_witness_witness_witness
  5. L43
    cases hh_witness_witness_witness_witness
  6. L44
    cases hh_witness_witness_witness_witness_right
  7. L45
    cases hh_witness_witness_witness_witness_right_right
  8. L46
    cases hh_witness_witness_witness_witness_right_right_right
07Establish hmL47–56

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cf convergent matrix successor elimination.

  1. L47
    have hm · expand full local formula (602 characters)have hm : ∃ cfc_tail_alignment_matrix. ∃ cfc_a_alignment_matrix. ∃ cfc_b_alignment_matrix. ∃ cfc_c_alignment_matrix. ∃ cfc_d_alignment_matrix. ∃ cfc_q_alignment_matrix. ConvergentMatrixTrace(cfc_tail_alignment_matrix,H,E,k,cfc_a_alignment_matrix,cfc_b_alignment_matrix,cfc_c_alignment_matrix,cfc_d_alignment_matrix) ∧ (ListCell(s,cfc_q_alignment_matrix,cfc_tail_alignment_matrix) ∧ (u = cfc_q_alignment_matrix · cfc_a_alignment_matrix + cfc_c_alignment_matrix ∧ (U = cfc_q_alignment_matrix · cfc_b_alignment_matrix + cfc_d_alignment_matrix ∧ (v = cfc_a_alignment_matrix ∧ V = cfc_b_alignment_matrix))))
    Definitions: ListCellConvergentMatrixTrace
  2. L48
    specialize cf_convergent_matrix_successor_elimination (s)
  3. L49
    specialize cf_convergent_matrix_successor_elimination (H)
  4. L50
    specialize cf_convergent_matrix_successor_elimination (E)
  5. L51
    specialize cf_convergent_matrix_successor_elimination (k)
  6. L52
    specialize cf_convergent_matrix_successor_elimination (u)
  7. L53
    specialize cf_convergent_matrix_successor_elimination (U)
  8. L54
    specialize cf_convergent_matrix_successor_elimination (v)
  9. L55
    specialize cf_convergent_matrix_successor_elimination (V)
  10. L56
    apply cf_convergent_matrix_successor_elimination
08Use earlier factsL57–57

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L57
    exact hnew
09Separate the logical casesL58–67

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L58
    cases hm
  2. L59
    cases hm_witness
  3. L60
    cases hm_witness_witness
  4. L61
    cases hm_witness_witness_witness
  5. L62
    cases hm_witness_witness_witness_witness
  6. L63
    cases hm_witness_witness_witness_witness_witness
  7. L64
    cases hm_witness_witness_witness_witness_witness_witness
  8. L65
    cases hm_witness_witness_witness_witness_witness_witness_right
  9. L66
    cases hm_witness_witness_witness_witness_witness_witness_right_right
  10. L67
    cases hm_witness_witness_witness_witness_witness_witness_right_right_right
10Separate the logical casesL68–68

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L68
    cases hm_witness_witness_witness_witness_witness_witness_right_right_right_right
11Establish heqL69–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply cell functional.

  1. L69
    have heq : x = x9 /\ x2 = x4
  2. L70
    specialize cell_functional (s)
  3. L71
    specialize cell_functional (x)
  4. L72
    specialize cell_functional (x2)
  5. L73
    specialize cell_functional (x9)
  6. L74
    specialize cell_functional (x4)
  7. L75
    apply cell_functional
  8. L76
    exact hh_witness_witness_witness_witness_right_right_right_left
  9. L77
    exact hm_witness_witness_witness_witness_witness_witness_right_left
12Separate the logical casesL78–78

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L78
    cases heq
13Construct an explicit witnessL79–86

Supply the displayed value, then prove that it has the required property.

  1. L79
    exists x1
  2. L80
    exists x2
  3. L81
    exists x3
  4. L82
    exists x9
  5. L83
    exists x5
  6. L84
    exists x6
  7. L85
    exists x7
  8. L86
    exists x8
14Separate the logical casesL87–87

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L87
    split
15Use earlier factsL88–88

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L88
    exact hh_witness_witness_witness_witness_left
16Separate the logical casesL89–89

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L89
    split
17Calculate and transport equalitiesL90–90

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L90
    rewrite <- heq_left
18Use earlier factsL91–91

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L91
    exact hh_witness_witness_witness_witness_right_left
19Separate the logical casesL92–92

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L92
    split
20Use earlier factsL93–93

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L93
    exact hh_witness_witness_witness_witness_right_right_left
21Separate the logical casesL94–94

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L94
    split
22Use earlier factsL95–95

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L95
    exact hh_witness_witness_witness_witness_right_right_right_right
23Separate the logical casesL96–96

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L96
    split
24Use earlier factsL97–106

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L97
    specialize cf_convergent_matrix_list_transport (x4)
  2. L98
    specialize cf_convergent_matrix_list_transport (x2)
  3. L99
    specialize cf_convergent_matrix_list_transport (H)
  4. L100
    specialize cf_convergent_matrix_list_transport (E)
  5. L101
    specialize cf_convergent_matrix_list_transport (k)
  6. L102
    specialize cf_convergent_matrix_list_transport (x5)
  7. L103
    specialize cf_convergent_matrix_list_transport (x6)
  8. L104
    specialize cf_convergent_matrix_list_transport (x7)
  9. L105
    specialize cf_convergent_matrix_list_transport (x8)
  10. L106
    apply cf_convergent_matrix_list_transport
25Calculate and transport equalitiesL107–107

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L107
    symm
26Use earlier factsL108–109

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L108
    exact heq_right
  2. L109
    exact hm_witness_witness_witness_witness_witness_witness_left
27Separate the logical casesL110–110

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L110
    split
28Use earlier factsL111–111

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L111
    exact hm_witness_witness_witness_witness_witness_witness_right_right_left
29Separate the logical casesL112–112

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L112
    split
30Use earlier factsL113–113

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L113
    exact hm_witness_witness_witness_witness_witness_witness_right_right_right_left
31Separate the logical casesL114–114

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L114
    split
32Use earlier factsL115–116

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L115
    exact hm_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  2. L116
    exact hm_witness_witness_witness_witness_witness_witness_right_right_right_right_right

Library-wide reading audit

Original exact command ledger · 116 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro s
  4. 0004intro h
  5. 0005intro e
  6. 0006intro L
  7. 0007intro H
  8. 0008intro E
  9. 0009intro k
  10. 0010intro u
  11. 0011intro U
  12. 0012intro v
  13. 0013intro V
  14. 0014intro hold
  15. 0015intro hnew
  16. 0016have hn : ~(s = 0)
  17. 0017intro hz
  18. 0018specialize cf_convergent_matrix_nonempty_list (s)
  19. 0019specialize cf_convergent_matrix_nonempty_list (H)
  20. 0020specialize cf_convergent_matrix_nonempty_list (E)
  21. 0021specialize cf_convergent_matrix_nonempty_list (k)
  22. 0022specialize cf_convergent_matrix_nonempty_list (u)
  23. 0023specialize cf_convergent_matrix_nonempty_list (U)
  24. 0024specialize cf_convergent_matrix_nonempty_list (v)
  25. 0025specialize cf_convergent_matrix_nonempty_list (V)
  26. 0026apply cf_convergent_matrix_nonempty_list
  27. 0027exact hnew
  28. 0028exact hz
  29. 0029have hh : exists cfc_q_alignment_head cfc_r_alignment_head cfc_tail_alignment_head cfc_length_alignment_head. (((L) = S cfc_length_alignment_head) /\ (((a) = (b) * cfc_q_alignment_head + cfc_r_alignment_head) /\ ((exists cfba_gap_alignment_headbound. cfba_gap_alignment_headbound + S (cfc_r_alignment_head) = (b)) /\ ((s = S ((cfc_q_alignment_head + cfc_tail_alignment_head) * S (cfc_q_alignment_head + cfc_tail_alignment_head) + (cfc_tail_alignment_head + cfc_tail_alignment_head))) /\ (exists cf_gcd_alignment_headhistory. ((((exists ff_h_cf_alignment_headhistory_initial_state. ff_h_cf_alignment_headhistory_initial_state + S (((cf_gcd_alignment_headhistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_headhistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))) = S ((S (0)) * e)) /\ exists ff_q_cf_alignment_headhistory_initial_state. h = ff_q_cf_alignment_headhistory_initial_state * S ((S (0)) * e) + (((cf_gcd_alignment_headhistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) * S ((cf_gcd_alignment_headhistory) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0)))) + ((((0) + (0)) * S ((0) + (0)) + ((0) + (0))) + (((0) + (0)) * S ((0) + (0)) + ((0) + (0))))))) /\ ((((exists ff_h_cf_alignment_headhistory_terminal_state. ff_h_cf_alignment_headhistory_terminal_state + S (((b) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head)))) * S ((b) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head)))) + ((((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head))) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head))))) = S ((S (cfc_length_alignment_head)) * e)) /\ exists ff_q_cf_alignment_headhistory_terminal_state. h = ff_q_cf_alignment_headhistory_terminal_state * S ((S (cfc_length_alignment_head)) * e) + (((b) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head)))) * S ((b) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head)))) + ((((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head))) + (((cfc_r_alignment_head) + (cfc_tail_alignment_head)) * S ((cfc_r_alignment_head) + (cfc_tail_alignment_head)) + ((cfc_tail_alignment_head) + (cfc_tail_alignment_head))))))) /\ forall cf_index_alignment_headhistory. (exists ff_lt_cf_alignment_headhistory_index. ff_lt_cf_alignment_headhistory_index + S cf_index_alignment_headhistory = cfc_length_alignment_head) -> exists cf_old_a_alignment_headhistory cf_old_b_alignment_headhistory cf_tail_alignment_headhistory cf_new_a_alignment_headhistory cf_new_b_alignment_headhistory cf_head_alignment_headhistory cf_quotient_alignment_headhistory. ((((exists ff_h_cf_alignment_headhistory_previous_state. ff_h_cf_alignment_headhistory_previous_state + S (((cf_old_a_alignment_headhistory) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory)))) * S ((cf_old_a_alignment_headhistory) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory)))) + ((((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory))) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory))))) = S ((S (cf_index_alignment_headhistory)) * e)) /\ exists ff_q_cf_alignment_headhistory_previous_state. h = ff_q_cf_alignment_headhistory_previous_state * S ((S (cf_index_alignment_headhistory)) * e) + (((cf_old_a_alignment_headhistory) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory)))) * S ((cf_old_a_alignment_headhistory) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory)))) + ((((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory))) + (((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) * S ((cf_old_b_alignment_headhistory) + (cf_tail_alignment_headhistory)) + ((cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory))))))) /\ ((((exists ff_h_cf_alignment_headhistory_following_state. ff_h_cf_alignment_headhistory_following_state + S (((cf_new_a_alignment_headhistory) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory)))) * S ((cf_new_a_alignment_headhistory) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory)))) + ((((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory))) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory))))) = S ((S (S cf_index_alignment_headhistory)) * e)) /\ exists ff_q_cf_alignment_headhistory_following_state. h = ff_q_cf_alignment_headhistory_following_state * S ((S (S cf_index_alignment_headhistory)) * e) + (((cf_new_a_alignment_headhistory) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory)))) * S ((cf_new_a_alignment_headhistory) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory)))) + ((((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory))) + (((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) * S ((cf_new_b_alignment_headhistory) + (cf_head_alignment_headhistory)) + ((cf_head_alignment_headhistory) + (cf_head_alignment_headhistory))))))) /\ (cf_new_b_alignment_headhistory = cf_old_a_alignment_headhistory /\ (cf_new_a_alignment_headhistory = cf_new_b_alignment_headhistory * cf_quotient_alignment_headhistory + cf_old_b_alignment_headhistory /\ ((exists ff_lt_cf_alignment_headhistory_remainder. ff_lt_cf_alignment_headhistory_remainder + S cf_old_b_alignment_headhistory = cf_new_b_alignment_headhistory) /\ (cf_head_alignment_headhistory = S ((cf_quotient_alignment_headhistory + cf_tail_alignment_headhistory) * S (cf_quotient_alignment_headhistory + cf_tail_alignment_headhistory) + (cf_tail_alignment_headhistory + cf_tail_alignment_headhistory)))))))))))))))
  30. 0030specialize cf_convergent_old_history_nonempty_head (a)
  31. 0031specialize cf_convergent_old_history_nonempty_head (b)
  32. 0032specialize cf_convergent_old_history_nonempty_head (s)
  33. 0033specialize cf_convergent_old_history_nonempty_head (h)
  34. 0034specialize cf_convergent_old_history_nonempty_head (e)
  35. 0035specialize cf_convergent_old_history_nonempty_head (L)
  36. 0036apply cf_convergent_old_history_nonempty_head
  37. 0037exact hold
  38. 0038exact hn
  39. 0039cases hh
  40. 0040cases hh_witness
  41. 0041cases hh_witness_witness
  42. 0042cases hh_witness_witness_witness
  43. 0043cases hh_witness_witness_witness_witness
  44. 0044cases hh_witness_witness_witness_witness_right
  45. 0045cases hh_witness_witness_witness_witness_right_right
  46. 0046cases hh_witness_witness_witness_witness_right_right_right
  47. 0047have hm : exists cfc_tail_alignment_matrix cfc_a_alignment_matrix cfc_b_alignment_matrix cfc_c_alignment_matrix cfc_d_alignment_matrix cfc_q_alignment_matrix. ((exists cfc_tail_alignment_matrixprefix. ((exists cfc_state_alignment_matrixprefixinitial. ((exists cfc_left_alignment_matrixprefixinitialcode cfc_right_alignment_matrixprefixinitialcode cfc_matrix_alignment_matrixprefixinitialcode. ((cfc_left_alignment_matrixprefixinitialcode = ((1) + (0)) * S ((1) + (0)) + ((0) + (0))) /\ ((cfc_right_alignment_matrixprefixinitialcode = ((0) + (1)) * S ((0) + (1)) + ((1) + (1))) /\ ((cfc_matrix_alignment_matrixprefixinitialcode = ((cfc_left_alignment_matrixprefixinitialcode) + (cfc_right_alignment_matrixprefixinitialcode)) * S ((cfc_left_alignment_matrixprefixinitialcode) + (cfc_right_alignment_matrixprefixinitialcode)) + ((cfc_right_alignment_matrixprefixinitialcode) + (cfc_right_alignment_matrixprefixinitialcode))) /\ ((cfc_state_alignment_matrixprefixinitial) = ((cfc_tail_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixinitialcode)) * S ((cfc_tail_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixinitialcode)) + ((cfc_matrix_alignment_matrixprefixinitialcode) + (cfc_matrix_alignment_matrixprefixinitialcode))))))) /\ (((exists ff_h_alignment_matrixprefixinitialentry. ff_h_alignment_matrixprefixinitialentry + S (cfc_state_alignment_matrixprefixinitial) = S ((S (0)) * E)) /\ exists ff_q_alignment_matrixprefixinitialentry. H = ff_q_alignment_matrixprefixinitialentry * S ((S (0)) * E) + (cfc_state_alignment_matrixprefixinitial))))) /\ ((exists cfc_state_alignment_matrixprefixterminal. ((exists cfc_left_alignment_matrixprefixterminalcode cfc_right_alignment_matrixprefixterminalcode cfc_matrix_alignment_matrixprefixterminalcode. ((cfc_left_alignment_matrixprefixterminalcode = ((cfc_a_alignment_matrix) + (cfc_b_alignment_matrix)) * S ((cfc_a_alignment_matrix) + (cfc_b_alignment_matrix)) + ((cfc_b_alignment_matrix) + (cfc_b_alignment_matrix))) /\ ((cfc_right_alignment_matrixprefixterminalcode = ((cfc_c_alignment_matrix) + (cfc_d_alignment_matrix)) * S ((cfc_c_alignment_matrix) + (cfc_d_alignment_matrix)) + ((cfc_d_alignment_matrix) + (cfc_d_alignment_matrix))) /\ ((cfc_matrix_alignment_matrixprefixterminalcode = ((cfc_left_alignment_matrixprefixterminalcode) + (cfc_right_alignment_matrixprefixterminalcode)) * S ((cfc_left_alignment_matrixprefixterminalcode) + (cfc_right_alignment_matrixprefixterminalcode)) + ((cfc_right_alignment_matrixprefixterminalcode) + (cfc_right_alignment_matrixprefixterminalcode))) /\ ((cfc_state_alignment_matrixprefixterminal) = ((cfc_tail_alignment_matrix) + (cfc_matrix_alignment_matrixprefixterminalcode)) * S ((cfc_tail_alignment_matrix) + (cfc_matrix_alignment_matrixprefixterminalcode)) + ((cfc_matrix_alignment_matrixprefixterminalcode) + (cfc_matrix_alignment_matrixprefixterminalcode))))))) /\ (((exists ff_h_alignment_matrixprefixterminalentry. ff_h_alignment_matrixprefixterminalentry + S (cfc_state_alignment_matrixprefixterminal) = S ((S (k)) * E)) /\ exists ff_q_alignment_matrixprefixterminalentry. H = ff_q_alignment_matrixprefixterminalentry * S ((S (k)) * E) + (cfc_state_alignment_matrixprefixterminal))))) /\ (forall cfc_index_alignment_matrixprefix. (exists cfba_gap_alignment_matrixprefixbound. cfba_gap_alignment_matrixprefixbound + S (cfc_index_alignment_matrixprefix) = (k)) -> exists cfc_old_alignment_matrixprefix cfc_a_alignment_matrixprefix cfc_b_alignment_matrixprefix cfc_c_alignment_matrixprefix cfc_d_alignment_matrixprefix cfc_new_alignment_matrixprefix cfc_quotient_alignment_matrixprefix. ((exists cfc_state_alignment_matrixprefixprevious. ((exists cfc_left_alignment_matrixprefixpreviouscode cfc_right_alignment_matrixprefixpreviouscode cfc_matrix_alignment_matrixprefixpreviouscode. ((cfc_left_alignment_matrixprefixpreviouscode = ((cfc_a_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix)) * S ((cfc_a_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix)) + ((cfc_b_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix))) /\ ((cfc_right_alignment_matrixprefixpreviouscode = ((cfc_c_alignment_matrixprefix) + (cfc_d_alignment_matrixprefix)) * S ((cfc_c_alignment_matrixprefix) + (cfc_d_alignment_matrixprefix)) + ((cfc_d_alignment_matrixprefix) + (cfc_d_alignment_matrixprefix))) /\ ((cfc_matrix_alignment_matrixprefixpreviouscode = ((cfc_left_alignment_matrixprefixpreviouscode) + (cfc_right_alignment_matrixprefixpreviouscode)) * S ((cfc_left_alignment_matrixprefixpreviouscode) + (cfc_right_alignment_matrixprefixpreviouscode)) + ((cfc_right_alignment_matrixprefixpreviouscode) + (cfc_right_alignment_matrixprefixpreviouscode))) /\ ((cfc_state_alignment_matrixprefixprevious) = ((cfc_old_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixpreviouscode)) * S ((cfc_old_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixpreviouscode)) + ((cfc_matrix_alignment_matrixprefixpreviouscode) + (cfc_matrix_alignment_matrixprefixpreviouscode))))))) /\ (((exists ff_h_alignment_matrixprefixpreviousentry. ff_h_alignment_matrixprefixpreviousentry + S (cfc_state_alignment_matrixprefixprevious) = S ((S (cfc_index_alignment_matrixprefix)) * E)) /\ exists ff_q_alignment_matrixprefixpreviousentry. H = ff_q_alignment_matrixprefixpreviousentry * S ((S (cfc_index_alignment_matrixprefix)) * E) + (cfc_state_alignment_matrixprefixprevious))))) /\ ((exists cfc_state_alignment_matrixprefixfollowing. ((exists cfc_left_alignment_matrixprefixfollowingcode cfc_right_alignment_matrixprefixfollowingcode cfc_matrix_alignment_matrixprefixfollowingcode. ((cfc_left_alignment_matrixprefixfollowingcode = (((cfc_quotient_alignment_matrixprefix * cfc_a_alignment_matrixprefix + cfc_c_alignment_matrixprefix)) + ((cfc_quotient_alignment_matrixprefix * cfc_b_alignment_matrixprefix + cfc_d_alignment_matrixprefix))) * S (((cfc_quotient_alignment_matrixprefix * cfc_a_alignment_matrixprefix + cfc_c_alignment_matrixprefix)) + ((cfc_quotient_alignment_matrixprefix * cfc_b_alignment_matrixprefix + cfc_d_alignment_matrixprefix))) + (((cfc_quotient_alignment_matrixprefix * cfc_b_alignment_matrixprefix + cfc_d_alignment_matrixprefix)) + ((cfc_quotient_alignment_matrixprefix * cfc_b_alignment_matrixprefix + cfc_d_alignment_matrixprefix)))) /\ ((cfc_right_alignment_matrixprefixfollowingcode = ((cfc_a_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix)) * S ((cfc_a_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix)) + ((cfc_b_alignment_matrixprefix) + (cfc_b_alignment_matrixprefix))) /\ ((cfc_matrix_alignment_matrixprefixfollowingcode = ((cfc_left_alignment_matrixprefixfollowingcode) + (cfc_right_alignment_matrixprefixfollowingcode)) * S ((cfc_left_alignment_matrixprefixfollowingcode) + (cfc_right_alignment_matrixprefixfollowingcode)) + ((cfc_right_alignment_matrixprefixfollowingcode) + (cfc_right_alignment_matrixprefixfollowingcode))) /\ ((cfc_state_alignment_matrixprefixfollowing) = ((cfc_new_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixfollowingcode)) * S ((cfc_new_alignment_matrixprefix) + (cfc_matrix_alignment_matrixprefixfollowingcode)) + ((cfc_matrix_alignment_matrixprefixfollowingcode) + (cfc_matrix_alignment_matrixprefixfollowingcode))))))) /\ (((exists ff_h_alignment_matrixprefixfollowingentry. ff_h_alignment_matrixprefixfollowingentry + S (cfc_state_alignment_matrixprefixfollowing) = S ((S (S cfc_index_alignment_matrixprefix)) * E)) /\ exists ff_q_alignment_matrixprefixfollowingentry. H = ff_q_alignment_matrixprefixfollowingentry * S ((S (S cfc_index_alignment_matrixprefix)) * E) + (cfc_state_alignment_matrixprefixfollowing))))) /\ (cfc_new_alignment_matrixprefix = S ((cfc_quotient_alignment_matrixprefix + cfc_old_alignment_matrixprefix) * S (cfc_quotient_alignment_matrixprefix + cfc_old_alignment_matrixprefix) + (cfc_old_alignment_matrixprefix + cfc_old_alignment_matrixprefix))))))))) /\ ((s = S ((cfc_q_alignment_matrix + cfc_tail_alignment_matrix) * S (cfc_q_alignment_matrix + cfc_tail_alignment_matrix) + (cfc_tail_alignment_matrix + cfc_tail_alignment_matrix))) /\ (((u) = cfc_q_alignment_matrix * cfc_a_alignment_matrix + cfc_c_alignment_matrix) /\ (((U) = cfc_q_alignment_matrix * cfc_b_alignment_matrix + cfc_d_alignment_matrix) /\ (((v) = cfc_a_alignment_matrix) /\ ((V) = cfc_b_alignment_matrix))))))
  48. 0048specialize cf_convergent_matrix_successor_elimination (s)
  49. 0049specialize cf_convergent_matrix_successor_elimination (H)
  50. 0050specialize cf_convergent_matrix_successor_elimination (E)
  51. 0051specialize cf_convergent_matrix_successor_elimination (k)
  52. 0052specialize cf_convergent_matrix_successor_elimination (u)
  53. 0053specialize cf_convergent_matrix_successor_elimination (U)
  54. 0054specialize cf_convergent_matrix_successor_elimination (v)
  55. 0055specialize cf_convergent_matrix_successor_elimination (V)
  56. 0056apply cf_convergent_matrix_successor_elimination
  57. 0057exact hnew
  58. 0058cases hm
  59. 0059cases hm_witness
  60. 0060cases hm_witness_witness
  61. 0061cases hm_witness_witness_witness
  62. 0062cases hm_witness_witness_witness_witness
  63. 0063cases hm_witness_witness_witness_witness_witness
  64. 0064cases hm_witness_witness_witness_witness_witness_witness
  65. 0065cases hm_witness_witness_witness_witness_witness_witness_right
  66. 0066cases hm_witness_witness_witness_witness_witness_witness_right_right
  67. 0067cases hm_witness_witness_witness_witness_witness_witness_right_right_right
  68. 0068cases hm_witness_witness_witness_witness_witness_witness_right_right_right_right
  69. 0069have heq : x = x9 /\ x2 = x4
  70. 0070specialize cell_functional (s)
  71. 0071specialize cell_functional (x)
  72. 0072specialize cell_functional (x2)
  73. 0073specialize cell_functional (x9)
  74. 0074specialize cell_functional (x4)
  75. 0075apply cell_functional
  76. 0076exact hh_witness_witness_witness_witness_right_right_right_left
  77. 0077exact hm_witness_witness_witness_witness_witness_witness_right_left
  78. 0078cases heq
  79. 0079exists x1
  80. 0080exists x2
  81. 0081exists x3
  82. 0082exists x9
  83. 0083exists x5
  84. 0084exists x6
  85. 0085exists x7
  86. 0086exists x8
  87. 0087split
  88. 0088exact hh_witness_witness_witness_witness_left
  89. 0089split
  90. 0090rewrite <- heq_left
  91. 0091exact hh_witness_witness_witness_witness_right_left
  92. 0092split
  93. 0093exact hh_witness_witness_witness_witness_right_right_left
  94. 0094split
  95. 0095exact hh_witness_witness_witness_witness_right_right_right_right
  96. 0096split
  97. 0097specialize cf_convergent_matrix_list_transport (x4)
  98. 0098specialize cf_convergent_matrix_list_transport (x2)
  99. 0099specialize cf_convergent_matrix_list_transport (H)
  100. 0100specialize cf_convergent_matrix_list_transport (E)
  101. 0101specialize cf_convergent_matrix_list_transport (k)
  102. 0102specialize cf_convergent_matrix_list_transport (x5)
  103. 0103specialize cf_convergent_matrix_list_transport (x6)
  104. 0104specialize cf_convergent_matrix_list_transport (x7)
  105. 0105specialize cf_convergent_matrix_list_transport (x8)
  106. 0106apply cf_convergent_matrix_list_transport
  107. 0107symm
  108. 0108exact heq_right
  109. 0109exact hm_witness_witness_witness_witness_witness_witness_left
  110. 0110split
  111. 0111exact hm_witness_witness_witness_witness_witness_witness_right_right_left
  112. 0112split
  113. 0113exact hm_witness_witness_witness_witness_witness_witness_right_right_right_left
  114. 0114split
  115. 0115exact hm_witness_witness_witness_witness_witness_witness_right_right_right_right_left
  116. 0116exact hm_witness_witness_witness_witness_witness_witness_right_right_right_right_right