Struct AbstractRefutation 

pub struct AbstractRefutation {
    pub rule_types: usize,
    pub invariant: &'static str,
    pub witness: CountingCert,
}

An abstract, scale-invariant refutation: the family’s rules symmetry-broken to their orbit types, plus the abstract invariant those types violate, plus the constant-size witness. For pigeonhole this is two rule-types (every pigeon takes a hole; no two share one) and the counting fact pigeons > holes — identical at every scale. This is the lift-and-shift-left: the proof’s true size is O(1) in the rule-types, reached by symmetry breaking the rules to their types, never by enumerating resolvents (the concrete and even the symmetric resolution closure both explode).

Fields

rule_types: usize

invariant: &'static str

witness: CountingCert

Trait Implementations

impl Clone for AbstractRefutation

fn clone(&self) -> AbstractRefutation

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for AbstractRefutation

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl PartialEq for AbstractRefutation

fn eq(&self, other: &AbstractRefutation) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for AbstractRefutation

impl StructuralPartialEq for AbstractRefutation