mc5.ivy

#lang ivy1.7

type t

relation p(X:t)


axiom X:t = 0 & Y = 0 -> X = Y
axiom X:t = Y & Y = 0 -> X = 0

invariant p(X)

after init {
    p(X) := true
}

action a(x:t)  = {
  p(x) := true
}


export a