fact: Definition checkTracef (e : Expr) (T : Trace) := match makeTriplets (norm e) with | tRC L r n => match fInT (getT (buildL L)) T with | true => match addEqMem (rArrayInit _ (fun r => class nil)) r rZFalse with | triple Ar1 true L1 => true | triple Ar1 false L1 => match evalTraceF T Ar1 with | triple Ar' false L => false | triple Ar' true L => true end end | false => false end end.
imports: Stalmarck(makeTriplet)