:: deftheorem Def5 defines Quantum_Mechanics-like QMAX_1:def 5 :
for IT being QM_Str holds
( IT is Quantum_Mechanics-like iff ( ( for A1, A2 being Element of Obs IT st ( for s being Element of Sts IT holds Meas (A1,s) = Meas (A2,s) ) holds
A1 = A2 ) & ( for s1, s2 being Element of Sts IT st ( for A being Element of Obs IT holds Meas (A,s1) = Meas (A,s2) ) holds
s1 = s2 ) & ( for s1, s2 being Element of Sts IT
for t being Real st 0 <= t & t <= 1 holds
ex s being Element of Sts IT st
for A being Element of Obs IT
for E being Event of Borel_Sets holds (Meas (A,s)) . E = (t * ((Meas (A,s1)) . E)) + ((1 - t) * ((Meas (A,s2)) . E)) ) ) );