Function lemma_serializer_congruent_symmetric

Source

pub proof fn lemma_serializer_congruent_symmetric<A, B>(a: A, b: B)where
    A: Consistency + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,
    B: Consistency<Val = A::Val> + SpecByteLen<T = A::Val> + SpecSerializer<SVal = A::Val>,

Expand description

requires

serializer_congruent(a, b),

ensures

serializer_congruent(b, a),

lemma_serializer_congruent_symmetric

Function lemma_serializer_congruent_symmetric Copy item path

Function lemma_serializer_congruent_symmetric