[prob_uniform_on_finite_set]
  ⊢ ∀ p. FINITE (p_space p) ∧ p_space p ̸= { } ∧
      events p = POW (p_space p) ∧
     (∀ s. s ∈ events p ⇒
     prob p s = &CARD s / &CARD (p_space p)) ⇒
     prob_space p

 [prob_space_word6p]
  ⊢ prob_space word6p

  [prob_space_word48p]
  ⊢ prob_space word48p

 [XcauseYF’_def]
 ⊢ ∀ X Y .
     XcauseYF’ X Y = prob word48p { x | S x ⊕ S (x ⊕ E X ) = Y }

 [XcauseYFkey_def]
  ⊢ ∀ X Y x.
     XcauseYFkey X Y x =
     (let x′= x ⊕ E X
      in prob word48p { k | S (x ⊕ k) ⊕ S (x′ ⊕ k) = Y })

  [XcauseYF_convert]
  ⊢ ∀ X Y x. XcauseYFkey X Y x = XcauseYF’ X Y

   [XcauseYFp_eq]
   ⊢ ∀ X Y .
       Xe = E X ∧ Xl = splitXF Xe ∧ Yl = splitYF Y ⇒
       XcauseYF’ X Y =
       Π (λ i. XcauseY (EL i Xl) (EL i Yl) (SBox (EL i S_data)))
       (count 8)

 [Skeys_def]

 [rc5keys_def]
  ⊢ ∀ r k.
     rc5keys r k =
     (let n = 3 × MAX (2 × (r + 1)) 2 in keys n r k)

 [RoundEn_def]

 [RoundDe_def]

 [RoundDe’_def]

 [RoundDe’_def]

 [RoundEe’_De’]
  ⊢ ∀ n b ki ki2. RoundDe’ n ki ki2 (RoundEn’ n ki ki2 b) = b