Function lemma_alt_serializer_congruence

Source

pub broadcast proof fn lemma_alt_serializer_congruence<A1, A2, B1, B2, const NONDETERMINISTIC: bool>(
    a: Alt<A1, B1, NONDETERMINISTIC>,
    b: Alt<A2, B2, NONDETERMINISTIC>,
)where
    A1: Consistency + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    A2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    B1: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,
    B2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val> + SpecSerializer<SVal = A1::Val>,

Expand description

requires

serializer_congruent(a.0, b.0),

serializer_congruent(a.1, b.1),

ensures

#[trigger] serializer_congruent(a, b),

lemma_alt_serializer_congruence

Function lemma_alt_serializer_congruence Copy item path

Function lemma_alt_serializer_congruence