CD0016

finite_bit_union_exists

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

Construct an actual beta characteristic union and a genuinely witnessed finite cardinality.

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 b c d e l n m. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((n)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((n)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> exists u v q. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((l))) * ff_v_fms_count) + ((q)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_summand. (u) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (v)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (l)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (v))) /\ exists ff_q_fms_count_decoded. (u) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (v)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (l)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * e)) /\ exists fs_q_fms_binary_right. d = fs_q_fms_binary_right * S ((S (fms_i_binary)) * e) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * v)) /\ exists fs_q_fms_binary_result. u = fs_q_fms_binary_result * S ((S (fms_i_binary)) * v) + (1)))))))

Constructive proof overview

Generated structural guide

Construct an actual beta characteristic union and a genuinely witnessed finite cardinality.

The unchanged tactic script uses 3 declared prerequisites and contains 87 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD0013 finite_bit_complement_exists CD0012 finite_bit_intersection_exists CD0015 finite_bit_union_of_complements

Direct dependents

CD002F finite_modular_sumset_prefix_exists CD0038 finite_modular_dyson_transform_exists

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

87 script commands · 16 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 (3)
finite bit complement existsfinite bit intersection existsfinite bit union of complements

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–9

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro n
  7. L7
    intro m
  8. L8
    intro hn
  9. L9
    intro hm
02Establish hAL10–16

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit complement exists.

  1. L10
    have hA : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ n + q = l)Definitions: LtBetaAtBitCount
  2. L11
    specialize finite_bit_complement_exists b
  3. L12
    specialize finite_bit_complement_exists c
  4. L13
    specialize finite_bit_complement_exists l
  5. L14
    specialize finite_bit_complement_exists n
  6. L15
    apply finite_bit_complement_exists
  7. L16
    exact hn
03Separate the logical casesL17–21

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

  1. L17
    cases hA
  2. L18
    cases hA_witness
  3. L19
    cases hA_witness_witness
  4. L20
    cases hA_witness_witness_witness
  5. L21
    cases hA_witness_witness_witness_right
04Establish hBL22–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit complement exists.

  1. L22
    have hB : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(d,e,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ m + q = l)Definitions: LtBetaAtBitCount
  2. L23
    specialize finite_bit_complement_exists d
  3. L24
    specialize finite_bit_complement_exists e
  4. L25
    specialize finite_bit_complement_exists l
  5. L26
    specialize finite_bit_complement_exists m
  6. L27
    apply finite_bit_complement_exists
  7. L28
    exact hm
05Separate the logical casesL29–33

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

  1. L29
    cases hB
  2. L30
    cases hB_witness
  3. L31
    cases hB_witness_witness
  4. L32
    cases hB_witness_witness_witness
  5. L33
    cases hB_witness_witness_witness_right
06Establish hIL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit intersection exists.

  1. L34
    have hI : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ModularSetIntersection(x,x1,x3,x4,u,v,l)Definitions: ModularSetIntersectionBitCount
  2. L35
    specialize finite_bit_intersection_exists x
  3. L36
    specialize finite_bit_intersection_exists x1
  4. L37
    specialize finite_bit_intersection_exists x3
  5. L38
    specialize finite_bit_intersection_exists x4
  6. L39
    specialize finite_bit_intersection_exists l
  7. L40
    specialize finite_bit_intersection_exists x2
  8. L41
    specialize finite_bit_intersection_exists x5
  9. L42
    apply finite_bit_intersection_exists
  10. L43
    exact hA_witness_witness_witness_left
07Use earlier factsL44–44

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

  1. L44
    exact hB_witness_witness_witness_left
08Separate the logical casesL45–48

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

  1. L45
    cases hI
  2. L46
    cases hI_witness
  3. L47
    cases hI_witness_witness
  4. L48
    cases hI_witness_witness_witness
09Establish hUL49–55

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit complement exists.

  1. L49
    have hU : ∃ u. ∃ v. ∃ q. BitCount(u,v,l,q) ∧ ((∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(x6,x7,x,y) → BetaAt(u,v,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) ∧ x8 + q = l)Definitions: LtBetaAtBitCount
  2. L50
    specialize finite_bit_complement_exists x6
  3. L51
    specialize finite_bit_complement_exists x7
  4. L52
    specialize finite_bit_complement_exists l
  5. L53
    specialize finite_bit_complement_exists x8
  6. L54
    apply finite_bit_complement_exists
  7. L55
    exact hI_witness_witness_witness_left
10Separate the logical casesL56–60

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

  1. L56
    cases hU
  2. L57
    cases hU_witness
  3. L58
    cases hU_witness_witness
  4. L59
    cases hU_witness_witness_witness
  5. L60
    cases hU_witness_witness_witness_right
11Construct an explicit witnessL61–63

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

  1. L61
    exists x9
  2. L62
    exists x10
  3. L63
    exists x11
12Separate the logical casesL64–64

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

  1. L64
    split
13Use earlier factsL65–65

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

  1. L65
    exact hU_witness_witness_witness_left
14Separate the logical casesL66–67

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

  1. L66
    cases hn
  2. L67
    cases hm
15Use earlier factsL68–77

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

  1. L68
    specialize finite_bit_union_of_complements b
  2. L69
    specialize finite_bit_union_of_complements c
  3. L70
    specialize finite_bit_union_of_complements d
  4. L71
    specialize finite_bit_union_of_complements e
  5. L72
    specialize finite_bit_union_of_complements x
  6. L73
    specialize finite_bit_union_of_complements x1
  7. L74
    specialize finite_bit_union_of_complements x3
  8. L75
    specialize finite_bit_union_of_complements x4
  9. L76
    specialize finite_bit_union_of_complements x6
  10. L77
    specialize finite_bit_union_of_complements x7
16Use earlier factsL78–87

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

  1. L78
    specialize finite_bit_union_of_complements x9
  2. L79
    specialize finite_bit_union_of_complements x10
  3. L80
    specialize finite_bit_union_of_complements l
  4. L81
    apply finite_bit_union_of_complements
  5. L82
    exact hn_right
  6. L83
    exact hm_right
  7. L84
    exact hA_witness_witness_witness_right_left
  8. L85
    exact hB_witness_witness_witness_right_left
  9. L86
    exact hI_witness_witness_witness_right
  10. L87
    exact hU_witness_witness_witness_right_left

Library-wide reading audit

Original exact command ledger · 87 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro n
  7. 0007intro m
  8. 0008intro hn
  9. 0009intro hm
  10. 0010have hA : exists u v q. (((exists ff_u_fms_hA ff_v_fms_hA. ((((exists ff_h_fms_hA_start. ff_h_fms_hA_start + S (0) = S ((S (0)) * ff_v_fms_hA)) /\ exists ff_q_fms_hA_start. ff_u_fms_hA = ff_q_fms_hA_start * S ((S (0)) * ff_v_fms_hA) + (0))) /\ ((((exists ff_h_fms_hA_terminal. ff_h_fms_hA_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_hA)) /\ exists ff_q_fms_hA_terminal. ff_u_fms_hA = ff_q_fms_hA_terminal * S ((S ((l))) * ff_v_fms_hA) + ((q)))) /\ forall ff_i_fms_hA. (exists ff_lt_fms_hA_bound. ff_lt_fms_hA_bound + S ff_i_fms_hA = (l)) -> exists ff_a_fms_hA ff_r_fms_hA ff_s_fms_hA. ((((exists ff_h_fms_hA_summand. ff_h_fms_hA_summand + S (ff_a_fms_hA) = S ((S (ff_i_fms_hA)) * (v))) /\ exists ff_q_fms_hA_summand. (u) = ff_q_fms_hA_summand * S ((S (ff_i_fms_hA)) * (v)) + (ff_a_fms_hA))) /\ ((((exists ff_h_fms_hA_partial. ff_h_fms_hA_partial + S (ff_r_fms_hA) = S ((S (ff_i_fms_hA)) * ff_v_fms_hA)) /\ exists ff_q_fms_hA_partial. ff_u_fms_hA = ff_q_fms_hA_partial * S ((S (ff_i_fms_hA)) * ff_v_fms_hA) + (ff_r_fms_hA))) /\ ((((exists ff_h_fms_hA_successor. ff_h_fms_hA_successor + S (ff_s_fms_hA) = S ((S (S ff_i_fms_hA)) * ff_v_fms_hA)) /\ exists ff_q_fms_hA_successor. ff_u_fms_hA = ff_q_fms_hA_successor * S ((S (S ff_i_fms_hA)) * ff_v_fms_hA) + (ff_s_fms_hA))) /\ ff_s_fms_hA = ff_r_fms_hA + ff_a_fms_hA)))))) /\ (forall ff_i_fms_hA. (exists ff_lt_fms_hA_bound. ff_lt_fms_hA_bound + S ff_i_fms_hA = (l)) -> exists ff_bit_fms_hA. ((((exists ff_h_fms_hA_decoded. ff_h_fms_hA_decoded + S (ff_bit_fms_hA) = S ((S (ff_i_fms_hA)) * (v))) /\ exists ff_q_fms_hA_decoded. (u) = ff_q_fms_hA_decoded * S ((S (ff_i_fms_hA)) * (v)) + (ff_bit_fms_hA))) /\ (ff_bit_fms_hA = 0 \/ ff_bit_fms_hA = 1))))) /\ ((forall fms_i_hA fms_a_hA fms_v_hA. (exists fms_gap_hA. fms_gap_hA + S (fms_i_hA) = (l)) -> (((exists fs_h_fms_hA_a. fs_h_fms_hA_a + S (fms_a_hA) = S ((S (fms_i_hA)) * c)) /\ exists fs_q_fms_hA_a. b = fs_q_fms_hA_a * S ((S (fms_i_hA)) * c) + (fms_a_hA))) -> (((exists fs_h_fms_hA_b. fs_h_fms_hA_b + S (fms_v_hA) = S ((S (fms_i_hA)) * v)) /\ exists fs_q_fms_hA_b. u = fs_q_fms_hA_b * S ((S (fms_i_hA)) * v) + (fms_v_hA))) -> ((fms_a_hA=0 /\ fms_v_hA=1) \/ (fms_a_hA=1 /\ fms_v_hA=0))) /\ n+q=l)
  11. 0011specialize finite_bit_complement_exists b
  12. 0012specialize finite_bit_complement_exists c
  13. 0013specialize finite_bit_complement_exists l
  14. 0014specialize finite_bit_complement_exists n
  15. 0015apply finite_bit_complement_exists
  16. 0016exact hn
  17. 0017cases hA
  18. 0018cases hA_witness
  19. 0019cases hA_witness_witness
  20. 0020cases hA_witness_witness_witness
  21. 0021cases hA_witness_witness_witness_right
  22. 0022have hB : exists u v q. (((exists ff_u_fms_hB ff_v_fms_hB. ((((exists ff_h_fms_hB_start. ff_h_fms_hB_start + S (0) = S ((S (0)) * ff_v_fms_hB)) /\ exists ff_q_fms_hB_start. ff_u_fms_hB = ff_q_fms_hB_start * S ((S (0)) * ff_v_fms_hB) + (0))) /\ ((((exists ff_h_fms_hB_terminal. ff_h_fms_hB_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_hB)) /\ exists ff_q_fms_hB_terminal. ff_u_fms_hB = ff_q_fms_hB_terminal * S ((S ((l))) * ff_v_fms_hB) + ((q)))) /\ forall ff_i_fms_hB. (exists ff_lt_fms_hB_bound. ff_lt_fms_hB_bound + S ff_i_fms_hB = (l)) -> exists ff_a_fms_hB ff_r_fms_hB ff_s_fms_hB. ((((exists ff_h_fms_hB_summand. ff_h_fms_hB_summand + S (ff_a_fms_hB) = S ((S (ff_i_fms_hB)) * (v))) /\ exists ff_q_fms_hB_summand. (u) = ff_q_fms_hB_summand * S ((S (ff_i_fms_hB)) * (v)) + (ff_a_fms_hB))) /\ ((((exists ff_h_fms_hB_partial. ff_h_fms_hB_partial + S (ff_r_fms_hB) = S ((S (ff_i_fms_hB)) * ff_v_fms_hB)) /\ exists ff_q_fms_hB_partial. ff_u_fms_hB = ff_q_fms_hB_partial * S ((S (ff_i_fms_hB)) * ff_v_fms_hB) + (ff_r_fms_hB))) /\ ((((exists ff_h_fms_hB_successor. ff_h_fms_hB_successor + S (ff_s_fms_hB) = S ((S (S ff_i_fms_hB)) * ff_v_fms_hB)) /\ exists ff_q_fms_hB_successor. ff_u_fms_hB = ff_q_fms_hB_successor * S ((S (S ff_i_fms_hB)) * ff_v_fms_hB) + (ff_s_fms_hB))) /\ ff_s_fms_hB = ff_r_fms_hB + ff_a_fms_hB)))))) /\ (forall ff_i_fms_hB. (exists ff_lt_fms_hB_bound. ff_lt_fms_hB_bound + S ff_i_fms_hB = (l)) -> exists ff_bit_fms_hB. ((((exists ff_h_fms_hB_decoded. ff_h_fms_hB_decoded + S (ff_bit_fms_hB) = S ((S (ff_i_fms_hB)) * (v))) /\ exists ff_q_fms_hB_decoded. (u) = ff_q_fms_hB_decoded * S ((S (ff_i_fms_hB)) * (v)) + (ff_bit_fms_hB))) /\ (ff_bit_fms_hB = 0 \/ ff_bit_fms_hB = 1))))) /\ ((forall fms_i_hB fms_a_hB fms_v_hB. (exists fms_gap_hB. fms_gap_hB + S (fms_i_hB) = (l)) -> (((exists fs_h_fms_hB_a. fs_h_fms_hB_a + S (fms_a_hB) = S ((S (fms_i_hB)) * e)) /\ exists fs_q_fms_hB_a. d = fs_q_fms_hB_a * S ((S (fms_i_hB)) * e) + (fms_a_hB))) -> (((exists fs_h_fms_hB_b. fs_h_fms_hB_b + S (fms_v_hB) = S ((S (fms_i_hB)) * v)) /\ exists fs_q_fms_hB_b. u = fs_q_fms_hB_b * S ((S (fms_i_hB)) * v) + (fms_v_hB))) -> ((fms_a_hB=0 /\ fms_v_hB=1) \/ (fms_a_hB=1 /\ fms_v_hB=0))) /\ m+q=l)
  23. 0023specialize finite_bit_complement_exists d
  24. 0024specialize finite_bit_complement_exists e
  25. 0025specialize finite_bit_complement_exists l
  26. 0026specialize finite_bit_complement_exists m
  27. 0027apply finite_bit_complement_exists
  28. 0028exact hm
  29. 0029cases hB
  30. 0030cases hB_witness
  31. 0031cases hB_witness_witness
  32. 0032cases hB_witness_witness_witness
  33. 0033cases hB_witness_witness_witness_right
  34. 0034have hI : exists u v q. (((exists ff_u_fms_union_inter ff_v_fms_union_inter. ((((exists ff_h_fms_union_inter_start. ff_h_fms_union_inter_start + S (0) = S ((S (0)) * ff_v_fms_union_inter)) /\ exists ff_q_fms_union_inter_start. ff_u_fms_union_inter = ff_q_fms_union_inter_start * S ((S (0)) * ff_v_fms_union_inter) + (0))) /\ ((((exists ff_h_fms_union_inter_terminal. ff_h_fms_union_inter_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_union_inter)) /\ exists ff_q_fms_union_inter_terminal. ff_u_fms_union_inter = ff_q_fms_union_inter_terminal * S ((S ((l))) * ff_v_fms_union_inter) + ((q)))) /\ forall ff_i_fms_union_inter. (exists ff_lt_fms_union_inter_bound. ff_lt_fms_union_inter_bound + S ff_i_fms_union_inter = (l)) -> exists ff_a_fms_union_inter ff_r_fms_union_inter ff_s_fms_union_inter. ((((exists ff_h_fms_union_inter_summand. ff_h_fms_union_inter_summand + S (ff_a_fms_union_inter) = S ((S (ff_i_fms_union_inter)) * (v))) /\ exists ff_q_fms_union_inter_summand. (u) = ff_q_fms_union_inter_summand * S ((S (ff_i_fms_union_inter)) * (v)) + (ff_a_fms_union_inter))) /\ ((((exists ff_h_fms_union_inter_partial. ff_h_fms_union_inter_partial + S (ff_r_fms_union_inter) = S ((S (ff_i_fms_union_inter)) * ff_v_fms_union_inter)) /\ exists ff_q_fms_union_inter_partial. ff_u_fms_union_inter = ff_q_fms_union_inter_partial * S ((S (ff_i_fms_union_inter)) * ff_v_fms_union_inter) + (ff_r_fms_union_inter))) /\ ((((exists ff_h_fms_union_inter_successor. ff_h_fms_union_inter_successor + S (ff_s_fms_union_inter) = S ((S (S ff_i_fms_union_inter)) * ff_v_fms_union_inter)) /\ exists ff_q_fms_union_inter_successor. ff_u_fms_union_inter = ff_q_fms_union_inter_successor * S ((S (S ff_i_fms_union_inter)) * ff_v_fms_union_inter) + (ff_s_fms_union_inter))) /\ ff_s_fms_union_inter = ff_r_fms_union_inter + ff_a_fms_union_inter)))))) /\ (forall ff_i_fms_union_inter. (exists ff_lt_fms_union_inter_bound. ff_lt_fms_union_inter_bound + S ff_i_fms_union_inter = (l)) -> exists ff_bit_fms_union_inter. ((((exists ff_h_fms_union_inter_decoded. ff_h_fms_union_inter_decoded + S (ff_bit_fms_union_inter) = S ((S (ff_i_fms_union_inter)) * (v))) /\ exists ff_q_fms_union_inter_decoded. (u) = ff_q_fms_union_inter_decoded * S ((S (ff_i_fms_union_inter)) * (v)) + (ff_bit_fms_union_inter))) /\ (ff_bit_fms_union_inter = 0 \/ ff_bit_fms_union_inter = 1))))) /\ (forall fms_i_union_inter. (exists fms_gap_union_inter. fms_gap_union_inter + S (fms_i_union_inter) = (l)) -> ((((((exists fs_h_fms_union_inter_result. fs_h_fms_union_inter_result + S (1) = S ((S (fms_i_union_inter)) * v)) /\ exists fs_q_fms_union_inter_result. u = fs_q_fms_union_inter_result * S ((S (fms_i_union_inter)) * v) + (1))) -> (((((exists fs_h_fms_union_inter_left. fs_h_fms_union_inter_left + S (1) = S ((S (fms_i_union_inter)) * x1)) /\ exists fs_q_fms_union_inter_left. x = fs_q_fms_union_inter_left * S ((S (fms_i_union_inter)) * x1) + (1))) /\ (((exists fs_h_fms_union_inter_right. fs_h_fms_union_inter_right + S (1) = S ((S (fms_i_union_inter)) * x4)) /\ exists fs_q_fms_union_inter_right. x3 = fs_q_fms_union_inter_right * S ((S (fms_i_union_inter)) * x4) + (1)))))) /\ ((((((exists fs_h_fms_union_inter_left. fs_h_fms_union_inter_left + S (1) = S ((S (fms_i_union_inter)) * x1)) /\ exists fs_q_fms_union_inter_left. x = fs_q_fms_union_inter_left * S ((S (fms_i_union_inter)) * x1) + (1))) /\ (((exists fs_h_fms_union_inter_right. fs_h_fms_union_inter_right + S (1) = S ((S (fms_i_union_inter)) * x4)) /\ exists fs_q_fms_union_inter_right. x3 = fs_q_fms_union_inter_right * S ((S (fms_i_union_inter)) * x4) + (1))))) -> (((exists fs_h_fms_union_inter_result. fs_h_fms_union_inter_result + S (1) = S ((S (fms_i_union_inter)) * v)) /\ exists fs_q_fms_union_inter_result. u = fs_q_fms_union_inter_result * S ((S (fms_i_union_inter)) * v) + (1)))))))
  35. 0035specialize finite_bit_intersection_exists x
  36. 0036specialize finite_bit_intersection_exists x1
  37. 0037specialize finite_bit_intersection_exists x3
  38. 0038specialize finite_bit_intersection_exists x4
  39. 0039specialize finite_bit_intersection_exists l
  40. 0040specialize finite_bit_intersection_exists x2
  41. 0041specialize finite_bit_intersection_exists x5
  42. 0042apply finite_bit_intersection_exists
  43. 0043exact hA_witness_witness_witness_left
  44. 0044exact hB_witness_witness_witness_left
  45. 0045cases hI
  46. 0046cases hI_witness
  47. 0047cases hI_witness_witness
  48. 0048cases hI_witness_witness_witness
  49. 0049have hU : exists u v q. (((exists ff_u_fms_union_final ff_v_fms_union_final. ((((exists ff_h_fms_union_final_start. ff_h_fms_union_final_start + S (0) = S ((S (0)) * ff_v_fms_union_final)) /\ exists ff_q_fms_union_final_start. ff_u_fms_union_final = ff_q_fms_union_final_start * S ((S (0)) * ff_v_fms_union_final) + (0))) /\ ((((exists ff_h_fms_union_final_terminal. ff_h_fms_union_final_terminal + S ((q)) = S ((S ((l))) * ff_v_fms_union_final)) /\ exists ff_q_fms_union_final_terminal. ff_u_fms_union_final = ff_q_fms_union_final_terminal * S ((S ((l))) * ff_v_fms_union_final) + ((q)))) /\ forall ff_i_fms_union_final. (exists ff_lt_fms_union_final_bound. ff_lt_fms_union_final_bound + S ff_i_fms_union_final = (l)) -> exists ff_a_fms_union_final ff_r_fms_union_final ff_s_fms_union_final. ((((exists ff_h_fms_union_final_summand. ff_h_fms_union_final_summand + S (ff_a_fms_union_final) = S ((S (ff_i_fms_union_final)) * (v))) /\ exists ff_q_fms_union_final_summand. (u) = ff_q_fms_union_final_summand * S ((S (ff_i_fms_union_final)) * (v)) + (ff_a_fms_union_final))) /\ ((((exists ff_h_fms_union_final_partial. ff_h_fms_union_final_partial + S (ff_r_fms_union_final) = S ((S (ff_i_fms_union_final)) * ff_v_fms_union_final)) /\ exists ff_q_fms_union_final_partial. ff_u_fms_union_final = ff_q_fms_union_final_partial * S ((S (ff_i_fms_union_final)) * ff_v_fms_union_final) + (ff_r_fms_union_final))) /\ ((((exists ff_h_fms_union_final_successor. ff_h_fms_union_final_successor + S (ff_s_fms_union_final) = S ((S (S ff_i_fms_union_final)) * ff_v_fms_union_final)) /\ exists ff_q_fms_union_final_successor. ff_u_fms_union_final = ff_q_fms_union_final_successor * S ((S (S ff_i_fms_union_final)) * ff_v_fms_union_final) + (ff_s_fms_union_final))) /\ ff_s_fms_union_final = ff_r_fms_union_final + ff_a_fms_union_final)))))) /\ (forall ff_i_fms_union_final. (exists ff_lt_fms_union_final_bound. ff_lt_fms_union_final_bound + S ff_i_fms_union_final = (l)) -> exists ff_bit_fms_union_final. ((((exists ff_h_fms_union_final_decoded. ff_h_fms_union_final_decoded + S (ff_bit_fms_union_final) = S ((S (ff_i_fms_union_final)) * (v))) /\ exists ff_q_fms_union_final_decoded. (u) = ff_q_fms_union_final_decoded * S ((S (ff_i_fms_union_final)) * (v)) + (ff_bit_fms_union_final))) /\ (ff_bit_fms_union_final = 0 \/ ff_bit_fms_union_final = 1))))) /\ ((forall fms_i_union_final fms_a_union_final fms_v_union_final. (exists fms_gap_union_final. fms_gap_union_final + S (fms_i_union_final) = (l)) -> (((exists fs_h_fms_union_final_a. fs_h_fms_union_final_a + S (fms_a_union_final) = S ((S (fms_i_union_final)) * x7)) /\ exists fs_q_fms_union_final_a. x6 = fs_q_fms_union_final_a * S ((S (fms_i_union_final)) * x7) + (fms_a_union_final))) -> (((exists fs_h_fms_union_final_b. fs_h_fms_union_final_b + S (fms_v_union_final) = S ((S (fms_i_union_final)) * v)) /\ exists fs_q_fms_union_final_b. u = fs_q_fms_union_final_b * S ((S (fms_i_union_final)) * v) + (fms_v_union_final))) -> ((fms_a_union_final=0 /\ fms_v_union_final=1) \/ (fms_a_union_final=1 /\ fms_v_union_final=0))) /\ x8+q=l)
  50. 0050specialize finite_bit_complement_exists x6
  51. 0051specialize finite_bit_complement_exists x7
  52. 0052specialize finite_bit_complement_exists l
  53. 0053specialize finite_bit_complement_exists x8
  54. 0054apply finite_bit_complement_exists
  55. 0055exact hI_witness_witness_witness_left
  56. 0056cases hU
  57. 0057cases hU_witness
  58. 0058cases hU_witness_witness
  59. 0059cases hU_witness_witness_witness
  60. 0060cases hU_witness_witness_witness_right
  61. 0061exists x9
  62. 0062exists x10
  63. 0063exists x11
  64. 0064split
  65. 0065exact hU_witness_witness_witness_left
  66. 0066cases hn
  67. 0067cases hm
  68. 0068specialize finite_bit_union_of_complements b
  69. 0069specialize finite_bit_union_of_complements c
  70. 0070specialize finite_bit_union_of_complements d
  71. 0071specialize finite_bit_union_of_complements e
  72. 0072specialize finite_bit_union_of_complements x
  73. 0073specialize finite_bit_union_of_complements x1
  74. 0074specialize finite_bit_union_of_complements x3
  75. 0075specialize finite_bit_union_of_complements x4
  76. 0076specialize finite_bit_union_of_complements x6
  77. 0077specialize finite_bit_union_of_complements x7
  78. 0078specialize finite_bit_union_of_complements x9
  79. 0079specialize finite_bit_union_of_complements x10
  80. 0080specialize finite_bit_union_of_complements l
  81. 0081apply finite_bit_union_of_complements
  82. 0082exact hn_right
  83. 0083exact hm_right
  84. 0084exact hA_witness_witness_witness_right_left
  85. 0085exact hB_witness_witness_witness_right_left
  86. 0086exact hI_witness_witness_witness_right
  87. 0087exact hU_witness_witness_witness_right_left