module native/canon
open native/a
open native/cw
open native/c
open native/common

-- Canonicalization facts to be optionally added in order to
-- eventually make checkings faster.

fact ax_AbWorld_canon {
	all a1, a2 : AbWorld | {
		a1.abAuthPurse = a2.abAuthPurse
		XiAbPurse (a1, a2, a1.abAuthPurse)
	} implies a1 = a2
}

fact ax_PayDetails_canon {
	from.~from & to.~to & fromSeqNo.~fromSeqNo & toSeqNo.~toSeqNo in iden	
}

fact ax_ConWorld_canon {
	all c1, c2 : ConWorld | {
		c1.conAuthPurse = c2.conAuthPurse
		XiConPurse (c1, c2, c1.conAuthPurse)
		c1.ether = c2.ether
		c1.archive = c2.archive
	} implies c1 = c2
}