Skip to main content

lemma_alt_prepare_congruence

vest_lib::combinators::congruence

Function lemma_alt_prepare_congruence 

Source 
pub broadcast proof fn lemma_alt_prepare_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>,
    A2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val>,
    B1: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val>,
    B2: Consistency<Val = A1::Val> + SpecByteLen<T = A1::Val>,
Expand description
requires
prepare_congruent(a.0, b.0),
prepare_congruent(a.1, b.1),
ensures
#[trigger] prepare_congruent(a, b),