--> a line starting with **> indicates a added/changed proof passage --> a line ending with * indicates a non-effective proof passage -- --> 1-init --> 1-want(s,k), c-want(s,k), i = k --> 1-want(s,k), c-want(s,k), ~(i = k), j = k --> 1-want(s,k), c-want(s,k), ~(i = k), ~(j = k), istep1 --> 1-want(s,k), ~c-want(s,k) --> 1-try(s,k), c-try(s,k), i = k, j = k --> 1-2-try(s,k), c-try(s,k), i = k, ~(j = k), inv2 --> 1-2-try(s,k), c-try(s,k), ~(i = k), j = k, inv2 --> 1-2-try(s,k), c-try(s,k), ~(i = k), ~(j = k) --> 1-try(s,k), ~c-try(s,k) --> 1-2-exit(s,k), c-exit(s,k), i = k --> 1-2-exit(s,k), c-exit(s,k), ~(i = k), j = k --> 1-2-exit(s,k), c-exit(s,k), ~(i = k), ~(j = k) --> 1-2-exit(s,k), ~c-exit(s,k) --> 2-init **> 2-2-want(s,k), c-want(s,k) * **> 2-2-want(s,k), ~c-want(s,k) **> 2-2-try(s,k), c-try(s,k) * **> 2-2-try(s,k), ~c-try(s,k) **> 2-2-exit(s,k), c-exit(s,k) * **> 2-2-exit(s,k), ~c-exit(s,k) --> Q.E.D --> 1-init open INV1 ops i j : -> Pid . -- |= red inv1(init,i,j) . close --> 1-want(s,k), c-want(s,k), i = k open INV1 -- arbitrary objects op s : -> Sys . ops i j k : -> Pid . -- assumptions eq inv1(s,I:Pid,J:Pid) = true . -- -- eq c-want(s,k) = true . eq pc(s,k) = rm . -- eq i = k . -- |= -- check if the predicate is true. red inv1(want(s,k),i,j) . close --> 1-want(s,k), c-want(s,k), ~(i = k), j = k open INV1 -- arbitrary objects op s : -> Sys . ops i j k : -> Pid . -- assumptions eq inv1(s,I:Pid,J:Pid) = true . -- -- eq c-want(s,k) = true . eq pc(s,k) = rm . -- eq (i = k) = false . eq j = k . -- |= -- check if the predicate is true. red inv1(want(s,k),i,j) . close --> 1-want(s,k), c-want(s,k), ~(i = k), ~(j = k), istep1 open ISTEP1 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- -- eq c-want(s,k) = true . eq pc(s,k) = rm . -- eq (i = k) = false . eq (j = k) = false . ** successor state eq s' = want(s,k) . -- |= ** check if the predicate is true. red istep1(i,j) . close --> 1-want(s,k), ~c-want(s,k) open INV1 -- arbitrary objects op s : -> Sys . ops i j k : -> Pid . -- assumptions eq inv1(s,I:Pid,J:Pid) = true . -- eq c-want(s,k) = false . -- |= -- check if the predicate is true. red inv1(want(s,k),i,j) . close --> 1-try(s,k), c-try(s,k), i = k, j = k open ISTEP1 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- -- eq c-try(s,k) = true . eq pc(s,k) = wt . eq top(queue(s)) = k . -- eq i = k . eq j = k . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-2-try(s,k), c-try(s,k), i = k, ~(j = k), inv2 open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-try(s,k) = true . eq pc(s,k) = wt . eq top(queue(s)) = k . -- eq i = k . eq (j = k) = false . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red inv2(s,j) implies istep1(i,j) . close --> 1-2-try(s,k), c-try(s,k), ~(i = k), j = k, inv2 open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-try(s,k) = true . eq pc(s,k) = wt . eq top(queue(s)) = k . -- eq (i = k) = false . eq j = k . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. ** TRANS inv2(s,i) from premises red inv2(s,i) implies istep1(i,j) . close --> 1-2-try(s,k), c-try(s,k), ~(i = k), ~(j = k) open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-try(s,k) = true . eq pc(s,k) = wt . eq top(queue(s)) = k . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-try(s,k), ~c-try(s,k) open ISTEP1 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq c-try(s,k) = false . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-2-exit(s,k), c-exit(s,k), i = k open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq i = k . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-2-exit(s,k), c-exit(s,k), ~(i = k), j = k open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq (i = k) = false . eq j = k . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-2-exit(s,k), c-exit(s,k), ~(i = k), ~(j = k) open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 1-2-exit(s,k), ~c-exit(s,k) open INV2 -- arbitrary objects ops i j k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,J:Pid) = true . -- eq c-exit(s,k) = false . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep1(i,j) . close --> 2-init open INV2 ops i : -> Pid . -- |= red inv2(init,i) . close --> 2-2-want(s,k), c-want(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- -- eq c-want(s,k) = true . eq pc(s,k) = rm . -- successor state eq s' = want(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> 2-2-want(s,k), ~c-want(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- eq c-want(s,k) = false . -- successor state eq s' = want(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> 2-2-try(s,k), c-try(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- -- eq c-try(s,k) = true . eq pc(s,k) = wt . eq top(queue(s)) = k . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> 2-2-try(s,k), ~c-try(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- eq c-try(s,k) = false . -- successor state eq s' = try(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> 2-2-exit(s,k), c-exit(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> 2-2-exit(s,k), ~c-exit(s,k) open ISTEP2 -- arbitrary objects ops i k : -> Pid . -- assumptions -- eq inv1(s,I:Pid,J:Pid) = true . -- eq inv2(s,I:Pid) = true . -- eq c-exit(s,k) = false . -- successor state eq s' = exit(s,k) . -- |= -- check if the predicate is true. red istep2(i) . close --> Q.E.D