--> I) Base cases open INV red inv2(init,i) . close --> II) Inductive cases --> 1 want(s,k) -- 1.1 c-want(s,k) = true open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq pc(s,i) = cs . eq top(queue(s)) = i . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq pc(s,i) = cs . eq top(queue(s)) = i . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq (pc(s,i) = cs) = false . eq top(queue(s)) = i . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq (pc(s,i) = cs) = false . eq top(queue(s)) = i . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq pc(s,i) = cs . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq pc(s,i) = cs . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq (pc(s,i) = cs) = false . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq (pc(s,i) = cs) = false . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = true . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq pc(s,i) = cs . eq top(queue(s)) = i . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq pc(s,i) = cs . eq top(queue(s)) = i . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq (pc(s,i) = cs) = false . eq top(queue(s)) = i . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq (pc(s,i) = cs) = false . eq top(queue(s)) = i . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq pc(s,i) = cs . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq pc(s,i) = cs . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq i = k . eq (pc(s,i) = cs) = false . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-want(s,k) = true . eq pc(s,k) = l1 . -- eq (i = k) = false . eq (pc(s,i) = cs) = false . eq (top(queue(s)) = i) = false . eq empty?(queue(s)) = false . -- successor eq s' = want(s,k) . -- checking red inv3(s,i) implies istep2(i) . close -- -- 1.2 c-want(s,k) = false open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-want(s,k) = false . -- successor eq s' = want(s,k) . -- checking red istep2(i) . close --> 2 try(s,k) -- 2.1 c-try(s,k) = true open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-try(s,k) = true . eq pc(s,k) = l2 . eq top(queue(s)) = k . -- eq i = k . -- successor eq s' = try(s,k) . -- checking red istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-try(s,k) = true . eq pc(s,k) = l2 . eq top(queue(s)) = k . -- eq (i = k) = false . -- successor eq s' = try(s,k) . -- checking red istep2(i) . close -- -- 2.2 c-try(s,k) = false open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-try(s,k) = false . -- successor eq s' = try(s,k) . -- checking red istep2(i) . close --> 3 exit(s,k) -- 3.1 c-exit(s,k) = true open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq i = k . eq pc(s,i) = cs . -- successor eq s' = exit(s,k) . -- checking red inv1(s,i,k) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq (i = k) = false . eq pc(s,i) = cs . -- successor eq s' = exit(s,k) . -- checking red inv1(s,i,k) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq i = k . eq (pc(s,i) = cs) = false . -- successor eq s' = exit(s,k) . -- checking red inv1(s,i,k) implies istep2(i) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq pc(s,k) = cs . -- eq (i = k) = false . eq (pc(s,i) = cs) = false . -- successor eq s' = exit(s,k) . -- checking red inv1(s,i,k) implies istep2(i) . close -- -- 3.2 c-exit(s,k) = false open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-exit(s,k) = false . -- successor eq s' = exit(s,k) . -- checking red istep2(i) . close --> Q.E.D.