structure A : Type

• n : ℕ

structure T : Type

• n : ℕ

instance instDecidableEqA : DecidableEq A

Equations

• One or more equations did not get rendered due to their size.

instance instDecidableEqT : DecidableEq T

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev AtomicOracle : Type

Equations

• AtomicOracle = (T → ℝ>0)

def diffmint (t0 t1 t0' t1' : T) : Prop

Equations

• diffmint t0 t1 t0' t1' = (t0 ≠ t0' ∧ t0 ≠ t1' ∨ t1 ≠ t0' ∧ t1 ≠ t1')

def samemint (t0 t1 t0' t1' : T) : Prop

Equations

• samemint t0 t1 t0' t1' = (t0 = t0' ∧ t1 = t1' ∨ t0 = t1' ∧ t1 = t0')

theorem switch_samemint (t0 t1 t0' t1' : T) (h : samemint t0 t1 t0' t1') : samemint t0' t1' t0 t1

instance instDecidableSamemint (t0 t1 t0' t1' : T) : Decidable (samemint t0 t1 t0' t1')

Equations

• instDecidableSamemint t0 t1 t0' t1' = id inferInstance

instance instDecidableDiffmint (t0 t1 t0' t1' : T) : Decidable (diffmint t0 t1 t0' t1')

Equations

• instDecidableDiffmint t0 t1 t0' t1' = id inferInstance

@[simp]

theorem not_diffmint_iff_samemint (t0 t1 t0' t1' : T) (hdif : t0 ≠ t1) : ¬diffmint t0 t1 t0' t1' ↔ samemint t0 t1 t0' t1'

@[simp]

theorem not_samemint_iff_diffmint (t0 t1 t0' t1' : T) (hdif : t0 ≠ t1) : ¬samemint t0 t1 t0' t1' ↔ diffmint t0 t1 t0' t1'

theorem self_samemint (t0 t1 : T) : samemint t0 t1 t0 t1

theorem samemint.iff_swap_inner_left (t0 t1 t0' t1' : T) : samemint t0 t1 t0' t1' ↔ samemint t1 t0 t0' t1'

theorem samemint.iff_swap_inner_right (t0 t1 t0' t1' : T) : samemint t0 t1 t0' t1' ↔ samemint t0 t1 t1' t0'

theorem samemint.iff_swap_inner (t0 t1 t0' t1' : T) : samemint t0 t1 t0' t1' ↔ samemint t1 t0 t1' t0'

theorem samemint.iff_swap_outer (t0 t1 t0' t1' : T) : samemint t0 t1 t0' t1' ↔ samemint t0' t1' t0 t1

theorem diffmint.iff_swap_inner_left (t0 t1 t0' t1' : T) : diffmint t0 t1 t0' t1' ↔ diffmint t1 t0 t0' t1'

theorem diffmint.iff_swap_inner_right (t0 t1 t0' t1' : T) : diffmint t0 t1 t0' t1' ↔ diffmint t0 t1 t1' t0'

theorem diffmint.iff_swap_inner (t0 t1 t0' t1' : T) : diffmint t0 t1 t0' t1' ↔ diffmint t1 t0 t1' t0'

theorem diffmint.iff_swap_outer (t0 t1 t0' t1' : T) (hdif1 : t0 ≠ t1) (hdif2 : t0' ≠ t1') : diffmint t0 t1 t0' t1' ↔ diffmint t0' t1' t0 t1

theorem diffmint.swap_inner {t0 t1 t0' t1' : T} (d : diffmint t0 t1 t0' t1') : diffmint t1 t0 t1' t0'

theorem diffmint.swap_inner_left {t0 t1 t0' t1' : T} (d : diffmint t0 t1 t0' t1') : diffmint t1 t0 t0' t1'