% For HTML
trace_equiv [Astate: TYPE,
A: [Astate -> Astate],
Istate: TYPE,
I: [Istate -> Istate],
Abst: (surjective?[Istate, Astate])]: THEORY
BEGIN
ASSUMING
Commutes: ASSUMPTION
FORALL (s: Istate): Abst(I(s)) = A(Abst(s))
ENDASSUMING
IMPORTING traces[Astate], traces[Istate]
r : VAR Astate
s : VAR Istate
Atrace(r): sequence[Astate] =
traces[Astate].trace(A, r)
Itrace(s): sequence[Istate] =
traces[Istate].trace(I, s)
trace_equiv_aux: LEMMA FORALL (i: nat):
map(Abst, Itrace(s))(i) = Atrace(Abst(s))(i)
trace_equiv: THEOREM map(Abst, Itrace(s)) = Atrace(Abst(s))
END trace_equiv