Vcgen1

include deduction

var p : bool

after init {
    p := true
}

export action a(q:bool) = {
    p := p | q;
}

invariant p

proof [this] {
    tactic vcgen;
    proof [initiation] {
        apply introNot
        apply elimNot with p = p
        property (p <-> true) proof {apply elimAndL with q = ~p}
        apply elimIffRev with q = true
        apply trivial
        apply elimAndR with p = p <-> true
    };
    proof [consecution] {
        apply introNot
        apply elimNot with p = p
        showgoals

let Z3 finish...

    }
}