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 PA statement
(forall bpt_a_seed bpt_e_seed. exists bpt_x_seed. (exists ff_b_bpt_value_seed ff_c_bpt_value_seed. ((forall ff_i_bpt_value_seed_repeat. (exists ff_lt_bpt_value_seed_repeat_bound. ff_lt_bpt_value_seed_repeat_bound + S ff_i_bpt_value_seed_repeat = bpt_e_seed) -> (((exists ff_h_bpt_value_seed_repeat_decoded. ff_h_bpt_value_seed_repeat_decoded + S (bpt_a_seed) = S ((S (ff_i_bpt_value_seed_repeat)) * ff_c_bpt_value_seed)) /\ exists ff_q_bpt_value_seed_repeat_decoded. ff_b_bpt_value_seed = ff_q_bpt_value_seed_repeat_decoded * S ((S (ff_i_bpt_value_seed_repeat)) * ff_c_bpt_value_seed) + (bpt_a_seed)))) /\ (exists ff_u_bpt_value_seed_product ff_v_bpt_value_seed_product. ((((exists ff_h_bpt_value_seed_product_start. ff_h_bpt_value_seed_product_start + S (1) = S ((S (0)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_start. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_start * S ((S (0)) * ff_v_bpt_value_seed_product) + (1))) /\ ((((exists ff_h_bpt_value_seed_product_terminal. ff_h_bpt_value_seed_product_terminal + S (bpt_x_seed) = S ((S (bpt_e_seed)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_terminal. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_terminal * S ((S (bpt_e_seed)) * ff_v_bpt_value_seed_product) + (bpt_x_seed))) /\ forall ff_i_bpt_value_seed_product. (exists ff_lt_bpt_value_seed_product_bound. ff_lt_bpt_value_seed_product_bound + S ff_i_bpt_value_seed_product = bpt_e_seed) -> exists ff_p_bpt_value_seed_product ff_r_bpt_value_seed_product ff_s_bpt_value_seed_product. ((((exists ff_h_bpt_value_seed_product_factor. ff_h_bpt_value_seed_product_factor + S (ff_p_bpt_value_seed_product) = S ((S (ff_i_bpt_value_seed_product)) * ff_c_bpt_value_seed)) /\ exists ff_q_bpt_value_seed_product_factor. ff_b_bpt_value_seed = ff_q_bpt_value_seed_product_factor * S ((S (ff_i_bpt_value_seed_product)) * ff_c_bpt_value_seed) + (ff_p_bpt_value_seed_product))) /\ ((((exists ff_h_bpt_value_seed_product_partial. ff_h_bpt_value_seed_product_partial + S (ff_r_bpt_value_seed_product) = S ((S (ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_partial. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_partial * S ((S (ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product) + (ff_r_bpt_value_seed_product))) /\ ((((exists ff_h_bpt_value_seed_product_successor. ff_h_bpt_value_seed_product_successor + S (ff_s_bpt_value_seed_product) = S ((S (S ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product)) /\ exists ff_q_bpt_value_seed_product_successor. ff_u_bpt_value_seed_product = ff_q_bpt_value_seed_product_successor * S ((S (S ff_i_bpt_value_seed_product)) * ff_v_bpt_value_seed_product) + (ff_s_bpt_value_seed_product))) /\ ff_s_bpt_value_seed_product = ff_r_bpt_value_seed_product * ff_p_bpt_value_seed_product))))))))) -> ((exists pa_b_bpt_seed_two pa_c_bpt_seed_two. ((forall pa_i_bpt_seed_two_repeat. (exists pa_lt_bpt_seed_two_repeat_bound. pa_lt_bpt_seed_two_repeat_bound + S pa_i_bpt_seed_two_repeat = 2) -> (((exists pa_h_bpt_seed_two_repeat_decoded. pa_h_bpt_seed_two_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_repeat_decoded. pa_b_bpt_seed_two = pa_q_bpt_seed_two_repeat_decoded * S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two) + (2)))) /\ (exists pa_u_bpt_seed_two_product pa_v_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_start. pa_h_bpt_seed_two_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_start. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_start * S ((S (0)) * pa_v_bpt_seed_two_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_product_terminal. pa_h_bpt_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_terminal. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_product) + (4))) /\ forall pa_i_bpt_seed_two_product. (exists pa_lt_bpt_seed_two_product_bound. pa_lt_bpt_seed_two_product_bound + S pa_i_bpt_seed_two_product = 2) -> exists pa_p_bpt_seed_two_product pa_r_bpt_seed_two_product pa_s_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_factor. pa_h_bpt_seed_two_product_factor + S (pa_p_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_product_factor. pa_b_bpt_seed_two = pa_q_bpt_seed_two_product_factor * S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two) + (pa_p_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_partial. pa_h_bpt_seed_two_product_partial + S (pa_r_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_partial. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_partial * S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_r_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_successor. pa_h_bpt_seed_two_product_successor + S (pa_s_bpt_seed_two_product) = S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_successor. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_successor * S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_s_bpt_seed_two_product))) /\ pa_s_bpt_seed_two_product = pa_r_bpt_seed_two_product * pa_p_bpt_seed_two_product)))))))) /\ (exists pa_b_bpt_seed_seven pa_c_bpt_seed_seven. ((forall pa_i_bpt_seed_seven_repeat. (exists pa_lt_bpt_seed_seven_repeat_bound. pa_lt_bpt_seed_seven_repeat_bound + S pa_i_bpt_seed_seven_repeat = 7) -> (((exists pa_h_bpt_seed_seven_repeat_decoded. pa_h_bpt_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_repeat_decoded. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_repeat_decoded * S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven) + (2)))) /\ (exists pa_u_bpt_seed_seven_product pa_v_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_start. pa_h_bpt_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_start. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_start * S ((S (0)) * pa_v_bpt_seed_seven_product) + (1))) /\ ((((exists pa_h_bpt_seed_seven_product_terminal. pa_h_bpt_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_terminal. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_terminal * S ((S (7)) * pa_v_bpt_seed_seven_product) + (128))) /\ forall pa_i_bpt_seed_seven_product. (exists pa_lt_bpt_seed_seven_product_bound. pa_lt_bpt_seed_seven_product_bound + S pa_i_bpt_seed_seven_product = 7) -> exists pa_p_bpt_seed_seven_product pa_r_bpt_seed_seven_product pa_s_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_factor. pa_h_bpt_seed_seven_product_factor + S (pa_p_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_product_factor. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_product_factor * S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven) + (pa_p_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_partial. pa_h_bpt_seed_seven_product_partial + S (pa_r_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_partial. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_partial * S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_r_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_successor. pa_h_bpt_seed_seven_product_successor + S (pa_s_bpt_seed_seven_product) = S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_successor. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_successor * S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_s_bpt_seed_seven_product))) /\ pa_s_bpt_seed_seven_product = pa_r_bpt_seed_seven_product * pa_p_bpt_seed_seven_product)))))))))Structural proof guide
One totality premise yields the exact seeds 2^2=4 and 2^7=128.
Direct prerequisites: pow_successor_compose_from_total, pow_two_base_two_value_four. The authored body proceeds by case analysis (1), intermediate claims (8), equality transport (204), closed numeral normalization (3).
Proof neighborhood
Direct dependencies
Direct dependents
BT00SW bertrand_h_six_step_transport_from_total BT00SX bertrand_j_six_step_transport_from_total BT00W5 pow_eleven_two_le_pow_two_seven_from_total BT00W6 pow_six_ten_le_pow_four_thirteen_from_total BT00WF pow_six_six_le_pow_four_eight_from_total BT00WG pow_six_four_le_pow_four_six_from_total BT00WI pow_two_double_eq_pow_four_from_totalFormal native tactic body
Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.
Read the argument
Proof checkpoints
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 (2)
01Fix variables and assumptionsL1–1
Work with arbitrary variables or the premises of the current implication.
- L1
intro htotal
02Establish htwo_existsL2–5
03Separate the logical casesL6–6
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L6
cases htwo_exists
04Establish htwo_valueL7–10
05Establish htwoL11–14
06Establish hthreeL15–23
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L15
have hthree : Pow(2,3,8)Definitions: Pow - L16
specialize pow_successor_compose_from_total 2 - L17
specialize pow_successor_compose_from_total 2 - L18
specialize pow_successor_compose_from_total 4 - L19
specialize pow_successor_compose_from_total 8 - L20
apply pow_successor_compose_from_total - L21
exact htotal - L22
exact htwo - L23
norm_num
07Establish hfourL24–32
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L24
have hfour : Pow(2,4,16)Definitions: Pow - L25
specialize pow_successor_compose_from_total 2 - L26
specialize pow_successor_compose_from_total 3 - L27
specialize pow_successor_compose_from_total 8 - L28
specialize pow_successor_compose_from_total 16 - L29
apply pow_successor_compose_from_total - L30
exact htotal - L31
exact hthree - L32
norm_num
08Establish hfiveL33–41
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L33
have hfive : Pow(2,5,32)Definitions: Pow - L34
specialize pow_successor_compose_from_total 2 - L35
specialize pow_successor_compose_from_total 4 - L36
specialize pow_successor_compose_from_total 16 - L37
specialize pow_successor_compose_from_total 32 - L38
apply pow_successor_compose_from_total - L39
exact htotal - L40
exact hfour - L41
norm_num
09Establish hsixL42–51
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L42
have hsix : Pow(2,6,64)Definitions: Pow - L43
specialize pow_successor_compose_from_total 2 - L44
specialize pow_successor_compose_from_total 5 - L45
specialize pow_successor_compose_from_total 32 - L46
specialize pow_successor_compose_from_total 64 - L47
apply pow_successor_compose_from_total - L48
exact htotal - L49
exact hfive - L50
symm - L51
rewrite PA6
10Calculate and transport equalitiesL52–61
11Calculate and transport equalitiesL62–71
12Calculate and transport equalitiesL72–81
13Calculate and transport equalitiesL82–91
14Calculate and transport equalitiesL92–101
15Calculate and transport equalitiesL102–111
16Calculate and transport equalitiesL112–120
17Establish hsevenL121–130
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply pow successor compose from total.
- L121
have hseven : Pow(2,7,128)Definitions: Pow - L122
specialize pow_successor_compose_from_total 2 - L123
specialize pow_successor_compose_from_total 6 - L124
specialize pow_successor_compose_from_total 64 - L125
specialize pow_successor_compose_from_total 128 - L126
apply pow_successor_compose_from_total - L127
exact htotal - L128
exact hsix - L129
symm - L130
rewrite PA6
18Calculate and transport equalitiesL131–140
19Calculate and transport equalitiesL141–150
20Calculate and transport equalitiesL151–160
21Calculate and transport equalitiesL161–170
22Calculate and transport equalitiesL171–180
23Calculate and transport equalitiesL181–190
24Calculate and transport equalitiesL191–200
25Calculate and transport equalitiesL201–210
26Calculate and transport equalitiesL211–220
27Calculate and transport equalitiesL221–230
28Calculate and transport equalitiesL231–240
29Calculate and transport equalitiesL241–250
30Calculate and transport equalitiesL251–260
31Calculate and transport equalitiesL261–263
32Separate the logical casesL264–264
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L264
split
Original exact command ledger · 266 lines
- 0001
intro htotal - 0002
have htwo_exists : exists x. (exists pa_b_bpt_seed_two_any pa_c_bpt_seed_two_any. ((forall pa_i_bpt_seed_two_any_repeat. (exists pa_lt_bpt_seed_two_any_repeat_bound. pa_lt_bpt_seed_two_any_repeat_bound + S pa_i_bpt_seed_two_any_repeat = 2) -> (((exists pa_h_bpt_seed_two_any_repeat_decoded. pa_h_bpt_seed_two_any_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_any_repeat)) * pa_c_bpt_seed_two_any)) /\ exists pa_q_bpt_seed_two_any_repeat_decoded. pa_b_bpt_seed_two_any = pa_q_bpt_seed_two_any_repeat_decoded * S ((S (pa_i_bpt_seed_two_any_repeat)) * pa_c_bpt_seed_two_any) + (2)))) /\ (exists pa_u_bpt_seed_two_any_product pa_v_bpt_seed_two_any_product. ((((exists pa_h_bpt_seed_two_any_product_start. pa_h_bpt_seed_two_any_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_start. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_start * S ((S (0)) * pa_v_bpt_seed_two_any_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_any_product_terminal. pa_h_bpt_seed_two_any_product_terminal + S (x) = S ((S (2)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_terminal. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_any_product) + (x))) /\ forall pa_i_bpt_seed_two_any_product. (exists pa_lt_bpt_seed_two_any_product_bound. pa_lt_bpt_seed_two_any_product_bound + S pa_i_bpt_seed_two_any_product = 2) -> exists pa_p_bpt_seed_two_any_product pa_r_bpt_seed_two_any_product pa_s_bpt_seed_two_any_product. ((((exists pa_h_bpt_seed_two_any_product_factor. pa_h_bpt_seed_two_any_product_factor + S (pa_p_bpt_seed_two_any_product) = S ((S (pa_i_bpt_seed_two_any_product)) * pa_c_bpt_seed_two_any)) /\ exists pa_q_bpt_seed_two_any_product_factor. pa_b_bpt_seed_two_any = pa_q_bpt_seed_two_any_product_factor * S ((S (pa_i_bpt_seed_two_any_product)) * pa_c_bpt_seed_two_any) + (pa_p_bpt_seed_two_any_product))) /\ ((((exists pa_h_bpt_seed_two_any_product_partial. pa_h_bpt_seed_two_any_product_partial + S (pa_r_bpt_seed_two_any_product) = S ((S (pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_partial. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_partial * S ((S (pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product) + (pa_r_bpt_seed_two_any_product))) /\ ((((exists pa_h_bpt_seed_two_any_product_successor. pa_h_bpt_seed_two_any_product_successor + S (pa_s_bpt_seed_two_any_product) = S ((S (S pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product)) /\ exists pa_q_bpt_seed_two_any_product_successor. pa_u_bpt_seed_two_any_product = pa_q_bpt_seed_two_any_product_successor * S ((S (S pa_i_bpt_seed_two_any_product)) * pa_v_bpt_seed_two_any_product) + (pa_s_bpt_seed_two_any_product))) /\ pa_s_bpt_seed_two_any_product = pa_r_bpt_seed_two_any_product * pa_p_bpt_seed_two_any_product)))))))) - 0003
specialize htotal 2 - 0004
specialize htotal 2 - 0005
exact htotal - 0006
cases htwo_exists - 0007
have htwo_value : x = 4 - 0008
specialize pow_two_base_two_value_four x - 0009
apply pow_two_base_two_value_four - 0010
exact htwo_exists_witness - 0011
have htwo : exists pa_b_bpt_seed_two pa_c_bpt_seed_two. ((forall pa_i_bpt_seed_two_repeat. (exists pa_lt_bpt_seed_two_repeat_bound. pa_lt_bpt_seed_two_repeat_bound + S pa_i_bpt_seed_two_repeat = 2) -> (((exists pa_h_bpt_seed_two_repeat_decoded. pa_h_bpt_seed_two_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_repeat_decoded. pa_b_bpt_seed_two = pa_q_bpt_seed_two_repeat_decoded * S ((S (pa_i_bpt_seed_two_repeat)) * pa_c_bpt_seed_two) + (2)))) /\ (exists pa_u_bpt_seed_two_product pa_v_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_start. pa_h_bpt_seed_two_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_start. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_start * S ((S (0)) * pa_v_bpt_seed_two_product) + (1))) /\ ((((exists pa_h_bpt_seed_two_product_terminal. pa_h_bpt_seed_two_product_terminal + S (4) = S ((S (2)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_terminal. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_terminal * S ((S (2)) * pa_v_bpt_seed_two_product) + (4))) /\ forall pa_i_bpt_seed_two_product. (exists pa_lt_bpt_seed_two_product_bound. pa_lt_bpt_seed_two_product_bound + S pa_i_bpt_seed_two_product = 2) -> exists pa_p_bpt_seed_two_product pa_r_bpt_seed_two_product pa_s_bpt_seed_two_product. ((((exists pa_h_bpt_seed_two_product_factor. pa_h_bpt_seed_two_product_factor + S (pa_p_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two)) /\ exists pa_q_bpt_seed_two_product_factor. pa_b_bpt_seed_two = pa_q_bpt_seed_two_product_factor * S ((S (pa_i_bpt_seed_two_product)) * pa_c_bpt_seed_two) + (pa_p_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_partial. pa_h_bpt_seed_two_product_partial + S (pa_r_bpt_seed_two_product) = S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_partial. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_partial * S ((S (pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_r_bpt_seed_two_product))) /\ ((((exists pa_h_bpt_seed_two_product_successor. pa_h_bpt_seed_two_product_successor + S (pa_s_bpt_seed_two_product) = S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product)) /\ exists pa_q_bpt_seed_two_product_successor. pa_u_bpt_seed_two_product = pa_q_bpt_seed_two_product_successor * S ((S (S pa_i_bpt_seed_two_product)) * pa_v_bpt_seed_two_product) + (pa_s_bpt_seed_two_product))) /\ pa_s_bpt_seed_two_product = pa_r_bpt_seed_two_product * pa_p_bpt_seed_two_product))))))) - 0012
rewrite <- htwo_value - 0013
rewrite <- htwo_value - 0014
exact htwo_exists_witness - 0015
have hthree : exists pa_b_bpt_seed_three pa_c_bpt_seed_three. ((forall pa_i_bpt_seed_three_repeat. (exists pa_lt_bpt_seed_three_repeat_bound. pa_lt_bpt_seed_three_repeat_bound + S pa_i_bpt_seed_three_repeat = 3) -> (((exists pa_h_bpt_seed_three_repeat_decoded. pa_h_bpt_seed_three_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_three_repeat)) * pa_c_bpt_seed_three)) /\ exists pa_q_bpt_seed_three_repeat_decoded. pa_b_bpt_seed_three = pa_q_bpt_seed_three_repeat_decoded * S ((S (pa_i_bpt_seed_three_repeat)) * pa_c_bpt_seed_three) + (2)))) /\ (exists pa_u_bpt_seed_three_product pa_v_bpt_seed_three_product. ((((exists pa_h_bpt_seed_three_product_start. pa_h_bpt_seed_three_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_start. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_start * S ((S (0)) * pa_v_bpt_seed_three_product) + (1))) /\ ((((exists pa_h_bpt_seed_three_product_terminal. pa_h_bpt_seed_three_product_terminal + S (8) = S ((S (3)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_terminal. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_terminal * S ((S (3)) * pa_v_bpt_seed_three_product) + (8))) /\ forall pa_i_bpt_seed_three_product. (exists pa_lt_bpt_seed_three_product_bound. pa_lt_bpt_seed_three_product_bound + S pa_i_bpt_seed_three_product = 3) -> exists pa_p_bpt_seed_three_product pa_r_bpt_seed_three_product pa_s_bpt_seed_three_product. ((((exists pa_h_bpt_seed_three_product_factor. pa_h_bpt_seed_three_product_factor + S (pa_p_bpt_seed_three_product) = S ((S (pa_i_bpt_seed_three_product)) * pa_c_bpt_seed_three)) /\ exists pa_q_bpt_seed_three_product_factor. pa_b_bpt_seed_three = pa_q_bpt_seed_three_product_factor * S ((S (pa_i_bpt_seed_three_product)) * pa_c_bpt_seed_three) + (pa_p_bpt_seed_three_product))) /\ ((((exists pa_h_bpt_seed_three_product_partial. pa_h_bpt_seed_three_product_partial + S (pa_r_bpt_seed_three_product) = S ((S (pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_partial. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_partial * S ((S (pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product) + (pa_r_bpt_seed_three_product))) /\ ((((exists pa_h_bpt_seed_three_product_successor. pa_h_bpt_seed_three_product_successor + S (pa_s_bpt_seed_three_product) = S ((S (S pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product)) /\ exists pa_q_bpt_seed_three_product_successor. pa_u_bpt_seed_three_product = pa_q_bpt_seed_three_product_successor * S ((S (S pa_i_bpt_seed_three_product)) * pa_v_bpt_seed_three_product) + (pa_s_bpt_seed_three_product))) /\ pa_s_bpt_seed_three_product = pa_r_bpt_seed_three_product * pa_p_bpt_seed_three_product))))))) - 0016
specialize pow_successor_compose_from_total 2 - 0017
specialize pow_successor_compose_from_total 2 - 0018
specialize pow_successor_compose_from_total 4 - 0019
specialize pow_successor_compose_from_total 8 - 0020
apply pow_successor_compose_from_total - 0021
exact htotal - 0022
exact htwo - 0023
norm_num - 0024
have hfour : exists pa_b_bpt_seed_four pa_c_bpt_seed_four. ((forall pa_i_bpt_seed_four_repeat. (exists pa_lt_bpt_seed_four_repeat_bound. pa_lt_bpt_seed_four_repeat_bound + S pa_i_bpt_seed_four_repeat = 4) -> (((exists pa_h_bpt_seed_four_repeat_decoded. pa_h_bpt_seed_four_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_four_repeat)) * pa_c_bpt_seed_four)) /\ exists pa_q_bpt_seed_four_repeat_decoded. pa_b_bpt_seed_four = pa_q_bpt_seed_four_repeat_decoded * S ((S (pa_i_bpt_seed_four_repeat)) * pa_c_bpt_seed_four) + (2)))) /\ (exists pa_u_bpt_seed_four_product pa_v_bpt_seed_four_product. ((((exists pa_h_bpt_seed_four_product_start. pa_h_bpt_seed_four_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_start. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_start * S ((S (0)) * pa_v_bpt_seed_four_product) + (1))) /\ ((((exists pa_h_bpt_seed_four_product_terminal. pa_h_bpt_seed_four_product_terminal + S (16) = S ((S (4)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_terminal. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_terminal * S ((S (4)) * pa_v_bpt_seed_four_product) + (16))) /\ forall pa_i_bpt_seed_four_product. (exists pa_lt_bpt_seed_four_product_bound. pa_lt_bpt_seed_four_product_bound + S pa_i_bpt_seed_four_product = 4) -> exists pa_p_bpt_seed_four_product pa_r_bpt_seed_four_product pa_s_bpt_seed_four_product. ((((exists pa_h_bpt_seed_four_product_factor. pa_h_bpt_seed_four_product_factor + S (pa_p_bpt_seed_four_product) = S ((S (pa_i_bpt_seed_four_product)) * pa_c_bpt_seed_four)) /\ exists pa_q_bpt_seed_four_product_factor. pa_b_bpt_seed_four = pa_q_bpt_seed_four_product_factor * S ((S (pa_i_bpt_seed_four_product)) * pa_c_bpt_seed_four) + (pa_p_bpt_seed_four_product))) /\ ((((exists pa_h_bpt_seed_four_product_partial. pa_h_bpt_seed_four_product_partial + S (pa_r_bpt_seed_four_product) = S ((S (pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_partial. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_partial * S ((S (pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product) + (pa_r_bpt_seed_four_product))) /\ ((((exists pa_h_bpt_seed_four_product_successor. pa_h_bpt_seed_four_product_successor + S (pa_s_bpt_seed_four_product) = S ((S (S pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product)) /\ exists pa_q_bpt_seed_four_product_successor. pa_u_bpt_seed_four_product = pa_q_bpt_seed_four_product_successor * S ((S (S pa_i_bpt_seed_four_product)) * pa_v_bpt_seed_four_product) + (pa_s_bpt_seed_four_product))) /\ pa_s_bpt_seed_four_product = pa_r_bpt_seed_four_product * pa_p_bpt_seed_four_product))))))) - 0025
specialize pow_successor_compose_from_total 2 - 0026
specialize pow_successor_compose_from_total 3 - 0027
specialize pow_successor_compose_from_total 8 - 0028
specialize pow_successor_compose_from_total 16 - 0029
apply pow_successor_compose_from_total - 0030
exact htotal - 0031
exact hthree - 0032
norm_num - 0033
have hfive : exists pa_b_bpt_seed_five pa_c_bpt_seed_five. ((forall pa_i_bpt_seed_five_repeat. (exists pa_lt_bpt_seed_five_repeat_bound. pa_lt_bpt_seed_five_repeat_bound + S pa_i_bpt_seed_five_repeat = 5) -> (((exists pa_h_bpt_seed_five_repeat_decoded. pa_h_bpt_seed_five_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_five_repeat)) * pa_c_bpt_seed_five)) /\ exists pa_q_bpt_seed_five_repeat_decoded. pa_b_bpt_seed_five = pa_q_bpt_seed_five_repeat_decoded * S ((S (pa_i_bpt_seed_five_repeat)) * pa_c_bpt_seed_five) + (2)))) /\ (exists pa_u_bpt_seed_five_product pa_v_bpt_seed_five_product. ((((exists pa_h_bpt_seed_five_product_start. pa_h_bpt_seed_five_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_start. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_start * S ((S (0)) * pa_v_bpt_seed_five_product) + (1))) /\ ((((exists pa_h_bpt_seed_five_product_terminal. pa_h_bpt_seed_five_product_terminal + S (32) = S ((S (5)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_terminal. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_terminal * S ((S (5)) * pa_v_bpt_seed_five_product) + (32))) /\ forall pa_i_bpt_seed_five_product. (exists pa_lt_bpt_seed_five_product_bound. pa_lt_bpt_seed_five_product_bound + S pa_i_bpt_seed_five_product = 5) -> exists pa_p_bpt_seed_five_product pa_r_bpt_seed_five_product pa_s_bpt_seed_five_product. ((((exists pa_h_bpt_seed_five_product_factor. pa_h_bpt_seed_five_product_factor + S (pa_p_bpt_seed_five_product) = S ((S (pa_i_bpt_seed_five_product)) * pa_c_bpt_seed_five)) /\ exists pa_q_bpt_seed_five_product_factor. pa_b_bpt_seed_five = pa_q_bpt_seed_five_product_factor * S ((S (pa_i_bpt_seed_five_product)) * pa_c_bpt_seed_five) + (pa_p_bpt_seed_five_product))) /\ ((((exists pa_h_bpt_seed_five_product_partial. pa_h_bpt_seed_five_product_partial + S (pa_r_bpt_seed_five_product) = S ((S (pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_partial. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_partial * S ((S (pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product) + (pa_r_bpt_seed_five_product))) /\ ((((exists pa_h_bpt_seed_five_product_successor. pa_h_bpt_seed_five_product_successor + S (pa_s_bpt_seed_five_product) = S ((S (S pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product)) /\ exists pa_q_bpt_seed_five_product_successor. pa_u_bpt_seed_five_product = pa_q_bpt_seed_five_product_successor * S ((S (S pa_i_bpt_seed_five_product)) * pa_v_bpt_seed_five_product) + (pa_s_bpt_seed_five_product))) /\ pa_s_bpt_seed_five_product = pa_r_bpt_seed_five_product * pa_p_bpt_seed_five_product))))))) - 0034
specialize pow_successor_compose_from_total 2 - 0035
specialize pow_successor_compose_from_total 4 - 0036
specialize pow_successor_compose_from_total 16 - 0037
specialize pow_successor_compose_from_total 32 - 0038
apply pow_successor_compose_from_total - 0039
exact htotal - 0040
exact hfour - 0041
norm_num - 0042
have hsix : exists pa_b_bpt_seed_six pa_c_bpt_seed_six. ((forall pa_i_bpt_seed_six_repeat. (exists pa_lt_bpt_seed_six_repeat_bound. pa_lt_bpt_seed_six_repeat_bound + S pa_i_bpt_seed_six_repeat = 6) -> (((exists pa_h_bpt_seed_six_repeat_decoded. pa_h_bpt_seed_six_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_six_repeat)) * pa_c_bpt_seed_six)) /\ exists pa_q_bpt_seed_six_repeat_decoded. pa_b_bpt_seed_six = pa_q_bpt_seed_six_repeat_decoded * S ((S (pa_i_bpt_seed_six_repeat)) * pa_c_bpt_seed_six) + (2)))) /\ (exists pa_u_bpt_seed_six_product pa_v_bpt_seed_six_product. ((((exists pa_h_bpt_seed_six_product_start. pa_h_bpt_seed_six_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_start. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_start * S ((S (0)) * pa_v_bpt_seed_six_product) + (1))) /\ ((((exists pa_h_bpt_seed_six_product_terminal. pa_h_bpt_seed_six_product_terminal + S (64) = S ((S (6)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_terminal. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_terminal * S ((S (6)) * pa_v_bpt_seed_six_product) + (64))) /\ forall pa_i_bpt_seed_six_product. (exists pa_lt_bpt_seed_six_product_bound. pa_lt_bpt_seed_six_product_bound + S pa_i_bpt_seed_six_product = 6) -> exists pa_p_bpt_seed_six_product pa_r_bpt_seed_six_product pa_s_bpt_seed_six_product. ((((exists pa_h_bpt_seed_six_product_factor. pa_h_bpt_seed_six_product_factor + S (pa_p_bpt_seed_six_product) = S ((S (pa_i_bpt_seed_six_product)) * pa_c_bpt_seed_six)) /\ exists pa_q_bpt_seed_six_product_factor. pa_b_bpt_seed_six = pa_q_bpt_seed_six_product_factor * S ((S (pa_i_bpt_seed_six_product)) * pa_c_bpt_seed_six) + (pa_p_bpt_seed_six_product))) /\ ((((exists pa_h_bpt_seed_six_product_partial. pa_h_bpt_seed_six_product_partial + S (pa_r_bpt_seed_six_product) = S ((S (pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_partial. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_partial * S ((S (pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product) + (pa_r_bpt_seed_six_product))) /\ ((((exists pa_h_bpt_seed_six_product_successor. pa_h_bpt_seed_six_product_successor + S (pa_s_bpt_seed_six_product) = S ((S (S pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product)) /\ exists pa_q_bpt_seed_six_product_successor. pa_u_bpt_seed_six_product = pa_q_bpt_seed_six_product_successor * S ((S (S pa_i_bpt_seed_six_product)) * pa_v_bpt_seed_six_product) + (pa_s_bpt_seed_six_product))) /\ pa_s_bpt_seed_six_product = pa_r_bpt_seed_six_product * pa_p_bpt_seed_six_product))))))) - 0043
specialize pow_successor_compose_from_total 2 - 0044
specialize pow_successor_compose_from_total 5 - 0045
specialize pow_successor_compose_from_total 32 - 0046
specialize pow_successor_compose_from_total 64 - 0047
apply pow_successor_compose_from_total - 0048
exact htotal - 0049
exact hfive - 0050
symm - 0051
rewrite PA6 - 0052
rewrite PA6 - 0053
rewrite PA5 - 0054
rewrite PA4 - 0055
rewrite PA4 - 0056
rewrite PA4 - 0057
rewrite PA4 - 0058
rewrite PA4 - 0059
rewrite PA4 - 0060
rewrite PA4 - 0061
rewrite PA4 - 0062
rewrite PA4 - 0063
rewrite PA4 - 0064
rewrite PA4 - 0065
rewrite PA4 - 0066
rewrite PA4 - 0067
rewrite PA4 - 0068
rewrite PA4 - 0069
rewrite PA4 - 0070
rewrite PA4 - 0071
rewrite PA4 - 0072
rewrite PA4 - 0073
rewrite PA4 - 0074
rewrite PA4 - 0075
rewrite PA4 - 0076
rewrite PA4 - 0077
rewrite PA4 - 0078
rewrite PA4 - 0079
rewrite PA4 - 0080
rewrite PA4 - 0081
rewrite PA4 - 0082
rewrite PA4 - 0083
rewrite PA4 - 0084
rewrite PA4 - 0085
rewrite PA4 - 0086
rewrite PA3 - 0087
rewrite PA4 - 0088
rewrite PA4 - 0089
rewrite PA4 - 0090
rewrite PA4 - 0091
rewrite PA4 - 0092
rewrite PA4 - 0093
rewrite PA4 - 0094
rewrite PA4 - 0095
rewrite PA4 - 0096
rewrite PA4 - 0097
rewrite PA4 - 0098
rewrite PA4 - 0099
rewrite PA4 - 0100
rewrite PA4 - 0101
rewrite PA4 - 0102
rewrite PA4 - 0103
rewrite PA4 - 0104
rewrite PA4 - 0105
rewrite PA4 - 0106
rewrite PA4 - 0107
rewrite PA4 - 0108
rewrite PA4 - 0109
rewrite PA4 - 0110
rewrite PA4 - 0111
rewrite PA4 - 0112
rewrite PA4 - 0113
rewrite PA4 - 0114
rewrite PA4 - 0115
rewrite PA4 - 0116
rewrite PA4 - 0117
rewrite PA4 - 0118
rewrite PA4 - 0119
rewrite PA3 - 0120
refl - 0121
have hseven : exists pa_b_bpt_seed_seven pa_c_bpt_seed_seven. ((forall pa_i_bpt_seed_seven_repeat. (exists pa_lt_bpt_seed_seven_repeat_bound. pa_lt_bpt_seed_seven_repeat_bound + S pa_i_bpt_seed_seven_repeat = 7) -> (((exists pa_h_bpt_seed_seven_repeat_decoded. pa_h_bpt_seed_seven_repeat_decoded + S (2) = S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_repeat_decoded. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_repeat_decoded * S ((S (pa_i_bpt_seed_seven_repeat)) * pa_c_bpt_seed_seven) + (2)))) /\ (exists pa_u_bpt_seed_seven_product pa_v_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_start. pa_h_bpt_seed_seven_product_start + S (1) = S ((S (0)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_start. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_start * S ((S (0)) * pa_v_bpt_seed_seven_product) + (1))) /\ ((((exists pa_h_bpt_seed_seven_product_terminal. pa_h_bpt_seed_seven_product_terminal + S (128) = S ((S (7)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_terminal. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_terminal * S ((S (7)) * pa_v_bpt_seed_seven_product) + (128))) /\ forall pa_i_bpt_seed_seven_product. (exists pa_lt_bpt_seed_seven_product_bound. pa_lt_bpt_seed_seven_product_bound + S pa_i_bpt_seed_seven_product = 7) -> exists pa_p_bpt_seed_seven_product pa_r_bpt_seed_seven_product pa_s_bpt_seed_seven_product. ((((exists pa_h_bpt_seed_seven_product_factor. pa_h_bpt_seed_seven_product_factor + S (pa_p_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven)) /\ exists pa_q_bpt_seed_seven_product_factor. pa_b_bpt_seed_seven = pa_q_bpt_seed_seven_product_factor * S ((S (pa_i_bpt_seed_seven_product)) * pa_c_bpt_seed_seven) + (pa_p_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_partial. pa_h_bpt_seed_seven_product_partial + S (pa_r_bpt_seed_seven_product) = S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_partial. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_partial * S ((S (pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_r_bpt_seed_seven_product))) /\ ((((exists pa_h_bpt_seed_seven_product_successor. pa_h_bpt_seed_seven_product_successor + S (pa_s_bpt_seed_seven_product) = S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product)) /\ exists pa_q_bpt_seed_seven_product_successor. pa_u_bpt_seed_seven_product = pa_q_bpt_seed_seven_product_successor * S ((S (S pa_i_bpt_seed_seven_product)) * pa_v_bpt_seed_seven_product) + (pa_s_bpt_seed_seven_product))) /\ pa_s_bpt_seed_seven_product = pa_r_bpt_seed_seven_product * pa_p_bpt_seed_seven_product))))))) - 0122
specialize pow_successor_compose_from_total 2 - 0123
specialize pow_successor_compose_from_total 6 - 0124
specialize pow_successor_compose_from_total 64 - 0125
specialize pow_successor_compose_from_total 128 - 0126
apply pow_successor_compose_from_total - 0127
exact htotal - 0128
exact hsix - 0129
symm - 0130
rewrite PA6 - 0131
rewrite PA6 - 0132
rewrite PA5 - 0133
rewrite PA4 - 0134
rewrite PA4 - 0135
rewrite PA4 - 0136
rewrite PA4 - 0137
rewrite PA4 - 0138
rewrite PA4 - 0139
rewrite PA4 - 0140
rewrite PA4 - 0141
rewrite PA4 - 0142
rewrite PA4 - 0143
rewrite PA4 - 0144
rewrite PA4 - 0145
rewrite PA4 - 0146
rewrite PA4 - 0147
rewrite PA4 - 0148
rewrite PA4 - 0149
rewrite PA4 - 0150
rewrite PA4 - 0151
rewrite PA4 - 0152
rewrite PA4 - 0153
rewrite PA4 - 0154
rewrite PA4 - 0155
rewrite PA4 - 0156
rewrite PA4 - 0157
rewrite PA4 - 0158
rewrite PA4 - 0159
rewrite PA4 - 0160
rewrite PA4 - 0161
rewrite PA4 - 0162
rewrite PA4 - 0163
rewrite PA4 - 0164
rewrite PA4 - 0165
rewrite PA4 - 0166
rewrite PA4 - 0167
rewrite PA4 - 0168
rewrite PA4 - 0169
rewrite PA4 - 0170
rewrite PA4 - 0171
rewrite PA4 - 0172
rewrite PA4 - 0173
rewrite PA4 - 0174
rewrite PA4 - 0175
rewrite PA4 - 0176
rewrite PA4 - 0177
rewrite PA4 - 0178
rewrite PA4 - 0179
rewrite PA4 - 0180
rewrite PA4 - 0181
rewrite PA4 - 0182
rewrite PA4 - 0183
rewrite PA4 - 0184
rewrite PA4 - 0185
rewrite PA4 - 0186
rewrite PA4 - 0187
rewrite PA4 - 0188
rewrite PA4 - 0189
rewrite PA4 - 0190
rewrite PA4 - 0191
rewrite PA4 - 0192
rewrite PA4 - 0193
rewrite PA4 - 0194
rewrite PA4 - 0195
rewrite PA4 - 0196
rewrite PA4 - 0197
rewrite PA3 - 0198
rewrite PA4 - 0199
rewrite PA4 - 0200
rewrite PA4 - 0201
rewrite PA4 - 0202
rewrite PA4 - 0203
rewrite PA4 - 0204
rewrite PA4 - 0205
rewrite PA4 - 0206
rewrite PA4 - 0207
rewrite PA4 - 0208
rewrite PA4 - 0209
rewrite PA4 - 0210
rewrite PA4 - 0211
rewrite PA4 - 0212
rewrite PA4 - 0213
rewrite PA4 - 0214
rewrite PA4 - 0215
rewrite PA4 - 0216
rewrite PA4 - 0217
rewrite PA4 - 0218
rewrite PA4 - 0219
rewrite PA4 - 0220
rewrite PA4 - 0221
rewrite PA4 - 0222
rewrite PA4 - 0223
rewrite PA4 - 0224
rewrite PA4 - 0225
rewrite PA4 - 0226
rewrite PA4 - 0227
rewrite PA4 - 0228
rewrite PA4 - 0229
rewrite PA4 - 0230
rewrite PA4 - 0231
rewrite PA4 - 0232
rewrite PA4 - 0233
rewrite PA4 - 0234
rewrite PA4 - 0235
rewrite PA4 - 0236
rewrite PA4 - 0237
rewrite PA4 - 0238
rewrite PA4 - 0239
rewrite PA4 - 0240
rewrite PA4 - 0241
rewrite PA4 - 0242
rewrite PA4 - 0243
rewrite PA4 - 0244
rewrite PA4 - 0245
rewrite PA4 - 0246
rewrite PA4 - 0247
rewrite PA4 - 0248
rewrite PA4 - 0249
rewrite PA4 - 0250
rewrite PA4 - 0251
rewrite PA4 - 0252
rewrite PA4 - 0253
rewrite PA4 - 0254
rewrite PA4 - 0255
rewrite PA4 - 0256
rewrite PA4 - 0257
rewrite PA4 - 0258
rewrite PA4 - 0259
rewrite PA4 - 0260
rewrite PA4 - 0261
rewrite PA4 - 0262
rewrite PA3 - 0263
refl - 0264
split - 0265
exact htwo - 0266
exact hseven