Skip to main content

lemma_serializer_congruent_transitive

vest_lib::combinators::congruence

Function lemma_serializer_congruent_transitive 

Source 
pub proof fn lemma_serializer_congruent_transitive<A, B, C>(a: A, b: B, c: C)
where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    C: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
Expand description
requires
serializer_congruent(a, b),
serializer_congruent(b, c),
ensures
serializer_congruent(a, c),