fact: Fixpoint evalTraceF (T : Trace) : rArray vM -> mbD := fun Ar => match T with | emptyTrace => triple _ _ _ Ar false nil | tripletTrace t => match doTripletF Ar t with | None => triple _ _ _ Ar false nil | Some T => T end | seqTrace T1 T2 => match evalTraceF T1 Ar with | triple Ar' true L' => triple _ _ _ Ar' true L' | triple Ar' false L' => appL L' (evalTraceF T2 Ar') end | dilemmaTrace a b T1 T2 => match addEqMem Ar a b with | triple Ar1 true L1 => match addEqMem Ar a (rZComp b) with | triple Ar2 true L2 => triple _ _ _ Ar true nil | triple Ar2 false L2 => appL L2 (evalTraceF T2 Ar2) end | triple Ar1 false L1 => match addEqMem Ar a (rZComp b) with | triple Ar2 true L2 => appL L1 (evalTraceF T1 Ar1) | triple Ar2 false L2 => match evalTraceF T1 Ar1 with | triple Ar1' true L1' => appL L2 (evalTraceF T2 Ar2) | triple Ar1' false L1' => match evalTraceF T2 Ar2 with | triple Ar2' true L2' => triple _ _ _ Ar1' false (appendRz L1 L1') | triple Ar2' false L2' => match interMem Ar1' Ar2' Ar (appendRz L1 L1') (appendRz L2 L2') with | (Ar', L') => triple _ _ _ Ar' false L' end end end end end end.
imports: Stalmarck(makeTriplet)