creusot_contracts::std::collections::hash_set

Function set_produces_trans

Source 
pub fn set_produces_trans<T: DeepModel, I: View<ViewTy = FSet<T::DeepModelTy>>>(
    a: I,
    ab: Seq<T>,
    b: I,
    bc: Seq<T>,
    c: I,
)
Expand description

logic

Seq::<T>::concat_contains();
proof_assert! { forall<i: Int, x: T> ab.len() <= i && ab.concat(bc).get(i) == Some(x) ==> bc.contains(x) };
proof_assert! { forall<i: Int> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] };

requires 

set_produces(a, ab, b)

requires 

set_produces(b, bc, c)

ensures 

set_produces(a, ab.concat(bc), c)