CD0015

finite_bit_union_of_complements

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

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

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.

Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ ab. ∀ ac. ∀ bb. ∀ bc. ∀ ib. ∀ ic. ∀ ub. ∀ uc. ∀ l. AllBits(b,c,l) → AllBits(d,e,l) → (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(b,c,x,y) → BetaAt(ab,ac,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) → (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(d,e,x,y) → BetaAt(bb,bc,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) → ModularSetIntersection(ab,ac,bb,bc,ib,ic,l) → (∀ x. ∀ y. ∀ z. Lt(x,l) → BetaAt(ib,ic,x,y) → BetaAt(ub,uc,x,z) → y = 0 ∧ z = 1 ∨ y = 1 ∧ z = 0) → ModularSetUnion(b,c,d,e,ub,uc,l)

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModularSetUnion(b,c,d,e,u,v,p) · 1ModularSetIntersection(b,c,d,e,u,v,p) · 1Lt(a,b) · 3BetaAt(b,c,i,x) · 31AllBits(b,c,l) · 2

Actual proof prerequisites

finite_bit_complement_member_ifffinite_bit_membership_decidable
Original expanded first-order 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)))))))

Complete tactic proof in conservative notation

All 110 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
finite bit complement member ifffinite bit membership decidable
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(ab,ac,i,1)BetaAt(b,c,i,1)Original native command in the exact edition
  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(bb,bc,i,1)BetaAt(d,e,i,1)Original native command in the exact edition
  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(ub,uc,i,1)BetaAt(ib,ic,i,1)Original native command in the exact edition
  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(ib,ic,i,1)BetaAt(ab,ac,i,1)BetaAt(bb,bc,i,1)Original native command in the exact edition
  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 : ¬BetaAt(ib,ic,i,1)Definitions: BetaAt(ib,ic,i,1)Original native command in the exact edition
  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 : BetaAt(b,c,i,1) ∨ ¬BetaAt(b,c,i,1)Definitions: BetaAt(b,c,i,1)Original native command in the exact edition
  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 : BetaAt(d,e,i,1) ∨ ¬BetaAt(d,e,i,1)Definitions: BetaAt(d,e,i,1)Original native command in the exact edition
  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 : BetaAt(ab,ac,i,1) ∧ BetaAt(bb,bc,i,1)Definitions: BetaAt(ab,ac,i,1)BetaAt(bb,bc,i,1)Original native command in the exact edition
  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 defined 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 : (BetaAt(ab,ac,i,1) → ¬BetaAt(b,c,i,1)) ∧ (¬BetaAt(b,c,i,1) → BetaAt(ab,ac,i,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 : (BetaAt(bb,bc,i,1) → ¬BetaAt(d,e,i,1)) ∧ (¬BetaAt(d,e,i,1) → BetaAt(bb,bc,i,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 : (BetaAt(ub,uc,i,1) → ¬BetaAt(ib,ic,i,1)) ∧ (¬BetaAt(ib,ic,i,1) → BetaAt(ub,uc,i,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 : (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))
  56. 0056specialize hinter i
  57. 0057apply hinter
  58. 0058exact hi
  59. 0059cases hpair
  60. 0060split
  61. 0061intro hu
  62. 0062have hnot : ¬BetaAt(ib,ic,i,1)
  63. 0063intro hx
  64. 0064apply hI_left
  65. 0065exact hu
  66. 0066exact hx
  67. 0067have hdA : BetaAt(b,c,i,1) ∨ ¬BetaAt(b,c,i,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 : BetaAt(d,e,i,1) ∨ ¬BetaAt(d,e,i,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 : BetaAt(ab,ac,i,1) ∧ BetaAt(bb,bc,i,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