Comp liveness1

type t
type u

schema admit = {
    relation p
    property p
}

var x : bool
var y : bool

var q : t
var r : u

temporal property [p1] globally ~x
proof {
    showgoals
    tactic l2s_full
    showgoals
    tactic mc
}

action a = {
    y := x;
}

after init {
    x := false;
    y := false;
    q := 0;
    r := 0;
}

export a

temporal property [p2] globally ~y
proof {

assume p1

    showgoals
    tactic l2s with
    invariant ~y & ~ (globally ~y) & ~($happened$ y) & (globally ~x)
    showgoals
}