CD0015

finite_bit_union_of_complements

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

Actual characteristic complements and intersection construct the exact union by decidable finite De Morgan reasoning.

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 ab ac bb bc ib ic ub uc l. (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (l)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (c))) /\ exists ff_q_fms_bits_decoded. (b) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (c)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (forall ff_i_fms_bits. (exists ff_lt_fms_bits_bound. ff_lt_fms_bits_bound + S ff_i_fms_bits = (l)) -> exists ff_bit_fms_bits. ((((exists ff_h_fms_bits_decoded. ff_h_fms_bits_decoded + S (ff_bit_fms_bits) = S ((S (ff_i_fms_bits)) * (e))) /\ exists ff_q_fms_bits_decoded. (d) = ff_q_fms_bits_decoded * S ((S (ff_i_fms_bits)) * (e)) + (ff_bit_fms_bits))) /\ (ff_bit_fms_bits = 0 \/ ff_bit_fms_bits = 1))) -> (forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * c)) /\ exists fs_q_fms_complement_a. b = fs_q_fms_complement_a * S ((S (fms_i_complement)) * c) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * ac)) /\ exists fs_q_fms_complement_b. ab = fs_q_fms_complement_b * S ((S (fms_i_complement)) * ac) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))) -> (forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * e)) /\ exists fs_q_fms_complement_a. d = fs_q_fms_complement_a * S ((S (fms_i_complement)) * e) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * bc)) /\ exists fs_q_fms_complement_b. bb = fs_q_fms_complement_b * S ((S (fms_i_complement)) * bc) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))) -> (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)) * ic)) /\ exists fs_q_fms_binary_result. ib = fs_q_fms_binary_result * S ((S (fms_i_binary)) * ic) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * ac)) /\ exists fs_q_fms_binary_left. ab = fs_q_fms_binary_left * S ((S (fms_i_binary)) * ac) + (1))) /\ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * bc)) /\ exists fs_q_fms_binary_right. bb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * bc) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * ac)) /\ exists fs_q_fms_binary_left. ab = fs_q_fms_binary_left * S ((S (fms_i_binary)) * ac) + (1))) /\ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * bc)) /\ exists fs_q_fms_binary_right. bb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * bc) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * ic)) /\ exists fs_q_fms_binary_result. ib = fs_q_fms_binary_result * S ((S (fms_i_binary)) * ic) + (1))))))) -> (forall fms_i_complement fms_a_complement fms_v_complement. (exists fms_gap_complement. fms_gap_complement + S (fms_i_complement) = (l)) -> (((exists fs_h_fms_complement_a. fs_h_fms_complement_a + S (fms_a_complement) = S ((S (fms_i_complement)) * ic)) /\ exists fs_q_fms_complement_a. ib = fs_q_fms_complement_a * S ((S (fms_i_complement)) * ic) + (fms_a_complement))) -> (((exists fs_h_fms_complement_b. fs_h_fms_complement_b + S (fms_v_complement) = S ((S (fms_i_complement)) * uc)) /\ exists fs_q_fms_complement_b. ub = fs_q_fms_complement_b * S ((S (fms_i_complement)) * uc) + (fms_v_complement))) -> ((fms_a_complement=0 /\ fms_v_complement=1) \/ (fms_a_complement=1 /\ fms_v_complement=0))) -> (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)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (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)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (1)))))))

Constructive proof overview

Generated structural guide

Actual characteristic complements and intersection construct the exact union by decidable finite De Morgan reasoning.

The unchanged tactic script uses 2 declared prerequisites and contains 110 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD0014 finite_bit_complement_member_iff CD0002 finite_bit_membership_decidable

Direct dependents

CD0016 finite_bit_union_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

110 script commands · 29 reading checkpoints · 8 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 (2)
finite bit complement member ifffinite bit membership decidable

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 b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro ib
  10. L10
    intro ic
02Fix variables and assumptionsL11–20

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

  1. L11
    intro ub
  2. L12
    intro uc
  3. L13
    intro l
  4. L14
    intro hbitsA
  5. L15
    intro hbitsB
  6. L16
    intro hcompA
  7. L17
    intro hcompB
  8. L18
    intro hinter
  9. L19
    intro hcompI
  10. L20
    intro i
03Fix variables and assumptionsL21–21

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

  1. L21
    intro hi
04Establish hAL22–31

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

  1. L22
    have hA : (BetaAt(ab,ac,i,1) → ¬BetaAt(b,c,i,1)) ∧ (¬BetaAt(b,c,i,1) → BetaAt(ab,ac,i,1))Definitions: BetaAt
  2. L23
    specialize finite_bit_complement_member_iff b
  3. L24
    specialize finite_bit_complement_member_iff c
  4. L25
    specialize finite_bit_complement_member_iff ab
  5. L26
    specialize finite_bit_complement_member_iff ac
  6. L27
    specialize finite_bit_complement_member_iff l
  7. L28
    specialize finite_bit_complement_member_iff i
  8. L29
    apply finite_bit_complement_member_iff
  9. L30
    exact hcompA
  10. L31
    exact hi
05Separate the logical casesL32–32

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

  1. L32
    cases hA
06Establish hBL33–42

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

  1. L33
    have hB : (BetaAt(bb,bc,i,1) → ¬BetaAt(d,e,i,1)) ∧ (¬BetaAt(d,e,i,1) → BetaAt(bb,bc,i,1))Definitions: BetaAt
  2. L34
    specialize finite_bit_complement_member_iff d
  3. L35
    specialize finite_bit_complement_member_iff e
  4. L36
    specialize finite_bit_complement_member_iff bb
  5. L37
    specialize finite_bit_complement_member_iff bc
  6. L38
    specialize finite_bit_complement_member_iff l
  7. L39
    specialize finite_bit_complement_member_iff i
  8. L40
    apply finite_bit_complement_member_iff
  9. L41
    exact hcompB
  10. L42
    exact hi
07Separate the logical casesL43–43

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

  1. L43
    cases hB
08Establish hIL44–53

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

  1. L44
    have hI : (BetaAt(ub,uc,i,1) → ¬BetaAt(ib,ic,i,1)) ∧ (¬BetaAt(ib,ic,i,1) → BetaAt(ub,uc,i,1))Definitions: BetaAt
  2. L45
    specialize finite_bit_complement_member_iff ib
  3. L46
    specialize finite_bit_complement_member_iff ic
  4. L47
    specialize finite_bit_complement_member_iff ub
  5. L48
    specialize finite_bit_complement_member_iff uc
  6. L49
    specialize finite_bit_complement_member_iff l
  7. L50
    specialize finite_bit_complement_member_iff i
  8. L51
    apply finite_bit_complement_member_iff
  9. L52
    exact hcompI
  10. L53
    exact hi
09Separate the logical casesL54–54

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

  1. L54
    cases hI
10Establish hpairL55–58

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

  1. L55
    have hpair : (BetaAt(ib,ic,i,1) → BetaAt(ab,ac,i,1) ∧ BetaAt(bb,bc,i,1)) ∧ (BetaAt(ab,ac,i,1) ∧ BetaAt(bb,bc,i,1) → BetaAt(ib,ic,i,1))Definitions: BetaAt
  2. L56
    specialize hinter i
  3. L57
    apply hinter
  4. L58
    exact hi
11Separate the logical casesL59–60

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

  1. L59
    cases hpair
  2. L60
    split
12Fix variables and assumptionsL61–61

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

  1. L61
    intro hu
13Establish hnotL62–66

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

  1. L62
    have hnot : ~(((exists fs_h_fms_union_notI. fs_h_fms_union_notI + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_union_notI. ib = fs_q_fms_union_notI * S ((S (i)) * ic) + (1)))
  2. L63
    intro hx
  3. L64
    apply hI_left
  4. L65
    exact hu
  5. L66
    exact hx
14Establish hdAL67–74

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

  1. L67
    have hdA : (((exists fs_h_fms_union_decA. fs_h_fms_union_decA + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_union_decA. b = fs_q_fms_union_decA * S ((S (i)) * c) + (1))) \/ ~(((exists fs_h_fms_union_decA. fs_h_fms_union_decA + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_union_decA. b = fs_q_fms_union_decA * S ((S (i)) * c) + (1)))
  2. L68
    specialize finite_bit_membership_decidable b
  3. L69
    specialize finite_bit_membership_decidable c
  4. L70
    specialize finite_bit_membership_decidable l
  5. L71
    specialize finite_bit_membership_decidable i
  6. L72
    apply finite_bit_membership_decidable
  7. L73
    exact hbitsA
  8. L74
    exact hi
15Separate the logical casesL75–76

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

  1. L75
    cases hdA
  2. L76
    left
16Use earlier factsL77–77

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

  1. L77
    exact hdA_left
17Establish hdBL78–85

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

  1. L78
    have hdB : (((exists fs_h_fms_union_decB. fs_h_fms_union_decB + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_union_decB. d = fs_q_fms_union_decB * S ((S (i)) * e) + (1))) \/ ~(((exists fs_h_fms_union_decB. fs_h_fms_union_decB + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_union_decB. d = fs_q_fms_union_decB * S ((S (i)) * e) + (1)))
  2. L79
    specialize finite_bit_membership_decidable d
  3. L80
    specialize finite_bit_membership_decidable e
  4. L81
    specialize finite_bit_membership_decidable l
  5. L82
    specialize finite_bit_membership_decidable i
  6. L83
    apply finite_bit_membership_decidable
  7. L84
    exact hbitsB
  8. L85
    exact hi
18Separate the logical casesL86–87

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

  1. L86
    cases hdB
  2. L87
    right
19Use earlier factsL88–88

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

  1. L88
    exact hdB_left
20Separate the logical casesL89–89

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

  1. L89
    exfalso
21Use earlier factsL90–91

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

  1. L90
    apply hnot
  2. L91
    apply hpair_right
22Separate the logical casesL92–92

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

  1. L92
    split
23Use earlier factsL93–96

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

  1. L93
    apply hA_right
  2. L94
    exact hdA_right
  3. L95
    apply hB_right
  4. L96
    exact hdB_right
24Fix variables and assumptionsL97–97

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

  1. L97
    intro hab
25Use earlier factsL98–98

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

  1. L98
    apply hI_right
26Fix variables and assumptionsL99–99

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

  1. L99
    intro hione
27Establish hbothL100–102

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

  1. L100
    have hboth : ((((exists fs_h_fms_union_CA. fs_h_fms_union_CA + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_union_CA. ab = fs_q_fms_union_CA * S ((S (i)) * ac) + (1))) /\ (((exists fs_h_fms_union_CB. fs_h_fms_union_CB + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_union_CB. bb = fs_q_fms_union_CB * S ((S (i)) * bc) + (1))))
  2. L101
    apply hpair_left
  3. L102
    exact hione
28Separate the logical casesL103–104

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

  1. L103
    cases hboth
  2. L104
    cases hab
29Use earlier factsL105–110

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

  1. L105
    apply hA_left
  2. L106
    exact hboth_left
  3. L107
    exact hab_left
  4. L108
    apply hB_left
  5. L109
    exact hboth_right
  6. L110
    exact hab_right

Library-wide reading audit

Original exact command ledger · 110 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro ib
  10. 0010intro ic
  11. 0011intro ub
  12. 0012intro uc
  13. 0013intro l
  14. 0014intro hbitsA
  15. 0015intro hbitsB
  16. 0016intro hcompA
  17. 0017intro hcompB
  18. 0018intro hinter
  19. 0019intro hcompI
  20. 0020intro i
  21. 0021intro hi
  22. 0022have hA : (((((exists fs_h_fms_hA_target. fs_h_fms_hA_target + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_hA_target. ab = fs_q_fms_hA_target * S ((S (i)) * ac) + (1))) -> (~(((exists fs_h_fms_hA_source. fs_h_fms_hA_source + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_hA_source. b = fs_q_fms_hA_source * S ((S (i)) * c) + (1))))) /\ ((~(((exists fs_h_fms_hA_source. fs_h_fms_hA_source + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_hA_source. b = fs_q_fms_hA_source * S ((S (i)) * c) + (1)))) -> (((exists fs_h_fms_hA_target. fs_h_fms_hA_target + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_hA_target. ab = fs_q_fms_hA_target * S ((S (i)) * ac) + (1)))))
  23. 0023specialize finite_bit_complement_member_iff b
  24. 0024specialize finite_bit_complement_member_iff c
  25. 0025specialize finite_bit_complement_member_iff ab
  26. 0026specialize finite_bit_complement_member_iff ac
  27. 0027specialize finite_bit_complement_member_iff l
  28. 0028specialize finite_bit_complement_member_iff i
  29. 0029apply finite_bit_complement_member_iff
  30. 0030exact hcompA
  31. 0031exact hi
  32. 0032cases hA
  33. 0033have hB : (((((exists fs_h_fms_hB_target. fs_h_fms_hB_target + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_hB_target. bb = fs_q_fms_hB_target * S ((S (i)) * bc) + (1))) -> (~(((exists fs_h_fms_hB_source. fs_h_fms_hB_source + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_hB_source. d = fs_q_fms_hB_source * S ((S (i)) * e) + (1))))) /\ ((~(((exists fs_h_fms_hB_source. fs_h_fms_hB_source + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_hB_source. d = fs_q_fms_hB_source * S ((S (i)) * e) + (1)))) -> (((exists fs_h_fms_hB_target. fs_h_fms_hB_target + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_hB_target. bb = fs_q_fms_hB_target * S ((S (i)) * bc) + (1)))))
  34. 0034specialize finite_bit_complement_member_iff d
  35. 0035specialize finite_bit_complement_member_iff e
  36. 0036specialize finite_bit_complement_member_iff bb
  37. 0037specialize finite_bit_complement_member_iff bc
  38. 0038specialize finite_bit_complement_member_iff l
  39. 0039specialize finite_bit_complement_member_iff i
  40. 0040apply finite_bit_complement_member_iff
  41. 0041exact hcompB
  42. 0042exact hi
  43. 0043cases hB
  44. 0044have hI : (((((exists fs_h_fms_hI_target. fs_h_fms_hI_target + S (1) = S ((S (i)) * uc)) /\ exists fs_q_fms_hI_target. ub = fs_q_fms_hI_target * S ((S (i)) * uc) + (1))) -> (~(((exists fs_h_fms_hI_source. fs_h_fms_hI_source + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_hI_source. ib = fs_q_fms_hI_source * S ((S (i)) * ic) + (1))))) /\ ((~(((exists fs_h_fms_hI_source. fs_h_fms_hI_source + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_hI_source. ib = fs_q_fms_hI_source * S ((S (i)) * ic) + (1)))) -> (((exists fs_h_fms_hI_target. fs_h_fms_hI_target + S (1) = S ((S (i)) * uc)) /\ exists fs_q_fms_hI_target. ub = fs_q_fms_hI_target * S ((S (i)) * uc) + (1)))))
  45. 0045specialize finite_bit_complement_member_iff ib
  46. 0046specialize finite_bit_complement_member_iff ic
  47. 0047specialize finite_bit_complement_member_iff ub
  48. 0048specialize finite_bit_complement_member_iff uc
  49. 0049specialize finite_bit_complement_member_iff l
  50. 0050specialize finite_bit_complement_member_iff i
  51. 0051apply finite_bit_complement_member_iff
  52. 0052exact hcompI
  53. 0053exact hi
  54. 0054cases hI
  55. 0055have hpair : (((((exists fs_h_fms_union_I. fs_h_fms_union_I + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_union_I. ib = fs_q_fms_union_I * S ((S (i)) * ic) + (1))) -> (((((exists fs_h_fms_union_CA. fs_h_fms_union_CA + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_union_CA. ab = fs_q_fms_union_CA * S ((S (i)) * ac) + (1))) /\ (((exists fs_h_fms_union_CB. fs_h_fms_union_CB + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_union_CB. bb = fs_q_fms_union_CB * S ((S (i)) * bc) + (1)))))) /\ ((((((exists fs_h_fms_union_CA. fs_h_fms_union_CA + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_union_CA. ab = fs_q_fms_union_CA * S ((S (i)) * ac) + (1))) /\ (((exists fs_h_fms_union_CB. fs_h_fms_union_CB + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_union_CB. bb = fs_q_fms_union_CB * S ((S (i)) * bc) + (1))))) -> (((exists fs_h_fms_union_I. fs_h_fms_union_I + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_union_I. ib = fs_q_fms_union_I * S ((S (i)) * ic) + (1)))))
  56. 0056specialize hinter i
  57. 0057apply hinter
  58. 0058exact hi
  59. 0059cases hpair
  60. 0060split
  61. 0061intro hu
  62. 0062have hnot : ~(((exists fs_h_fms_union_notI. fs_h_fms_union_notI + S (1) = S ((S (i)) * ic)) /\ exists fs_q_fms_union_notI. ib = fs_q_fms_union_notI * S ((S (i)) * ic) + (1)))
  63. 0063intro hx
  64. 0064apply hI_left
  65. 0065exact hu
  66. 0066exact hx
  67. 0067have hdA : (((exists fs_h_fms_union_decA. fs_h_fms_union_decA + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_union_decA. b = fs_q_fms_union_decA * S ((S (i)) * c) + (1))) \/ ~(((exists fs_h_fms_union_decA. fs_h_fms_union_decA + S (1) = S ((S (i)) * c)) /\ exists fs_q_fms_union_decA. b = fs_q_fms_union_decA * S ((S (i)) * c) + (1)))
  68. 0068specialize finite_bit_membership_decidable b
  69. 0069specialize finite_bit_membership_decidable c
  70. 0070specialize finite_bit_membership_decidable l
  71. 0071specialize finite_bit_membership_decidable i
  72. 0072apply finite_bit_membership_decidable
  73. 0073exact hbitsA
  74. 0074exact hi
  75. 0075cases hdA
  76. 0076left
  77. 0077exact hdA_left
  78. 0078have hdB : (((exists fs_h_fms_union_decB. fs_h_fms_union_decB + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_union_decB. d = fs_q_fms_union_decB * S ((S (i)) * e) + (1))) \/ ~(((exists fs_h_fms_union_decB. fs_h_fms_union_decB + S (1) = S ((S (i)) * e)) /\ exists fs_q_fms_union_decB. d = fs_q_fms_union_decB * S ((S (i)) * e) + (1)))
  79. 0079specialize finite_bit_membership_decidable d
  80. 0080specialize finite_bit_membership_decidable e
  81. 0081specialize finite_bit_membership_decidable l
  82. 0082specialize finite_bit_membership_decidable i
  83. 0083apply finite_bit_membership_decidable
  84. 0084exact hbitsB
  85. 0085exact hi
  86. 0086cases hdB
  87. 0087right
  88. 0088exact hdB_left
  89. 0089exfalso
  90. 0090apply hnot
  91. 0091apply hpair_right
  92. 0092split
  93. 0093apply hA_right
  94. 0094exact hdA_right
  95. 0095apply hB_right
  96. 0096exact hdB_right
  97. 0097intro hab
  98. 0098apply hI_right
  99. 0099intro hione
  100. 0100have hboth : ((((exists fs_h_fms_union_CA. fs_h_fms_union_CA + S (1) = S ((S (i)) * ac)) /\ exists fs_q_fms_union_CA. ab = fs_q_fms_union_CA * S ((S (i)) * ac) + (1))) /\ (((exists fs_h_fms_union_CB. fs_h_fms_union_CB + S (1) = S ((S (i)) * bc)) /\ exists fs_q_fms_union_CB. bb = fs_q_fms_union_CB * S ((S (i)) * bc) + (1))))
  101. 0101apply hpair_left
  102. 0102exact hione
  103. 0103cases hboth
  104. 0104cases hab
  105. 0105apply hA_left
  106. 0106exact hboth_left
  107. 0107exact hab_left
  108. 0108apply hB_left
  109. 0109exact hboth_right
  110. 0110exact hab_right