--> Base case open INV red inv2(init,i,j) . close --> Inductive cases --> 1 try(s,k) -- 1.1 c-try(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-try(s,k) = true . eq loc(s,k) = a . -- eq i = k . -- successor state eq s' = try(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-try(s,k) = true . eq loc(s,k) = a . -- eq j = k . -- successor state eq s' = try(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-try(s,k) = true . eq loc(s,k) = a . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = try(s,k) . -- check red istep2(i,j) . close -- -- 1.2 not c-try(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-try(s,k) = false . -- successor state eq s' = try(s,k) . -- check red istep2(i,j) . close --> 2 test(s,k) -- 2.1 c-test(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-test(s,k) = true . eq loc(s,k) = b . eq turn(s) = nop . -- eq i = k . -- successor state eq s' = test(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-test(s,k) = true . eq loc(s,k) = b . eq turn(s) = nop . -- eq (i = k) = false . -- successor state eq s' = test(s,k) . -- check red istep2(i,j) . close -- -- 2.2 not c-test(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-test(s,k) = false . -- successor state eq s' = test(s,k) . -- check red istep2(i,j) . close --> 3 set(s,k) -- 3.1 c-set(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-set(s,k) = true . eq loc(s,k) = c . -- eq i = k . eq j = k . -- successor state eq s' = set(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-set(s,k) = true . eq loc(s,k) = c . -- eq i = k . eq (j = k) = false . eq loc(s,j) = c . -- successor state eq s' = set(s,k) . -- check red inv3(s,j) implies istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-set(s,k) = true . eq loc(s,k) = c . -- eq i = k . eq (j = k) = false . eq (loc(s,j) = c) = false . -- successor state eq s' = set(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-set(s,k) = true . eq loc(s,k) = c . -- eq (i = k) = false . eq j = k . -- successor state eq s' = set(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-set(s,k) = true . eq loc(s,k) = c . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = set(s,k) . -- check red istep2(i,j) . close -- -- 3.2 not c-set(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-set(s,k) = false . -- successor state eq s' = set(s,k) . -- check red istep2(i,j) . close --> 4 check(s,k) -- 4.1 c-check(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-check(s,k) = true . eq loc(s,k) = d . eq l(s,k) <= now(s) = true . -- eq i = k . eq turn(s) = k . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-check(s,k) = true . eq loc(s,k) = d . eq l(s,k) <= now(s) = true . -- eq i = k . eq (turn(s) = k) = false . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-check(s,k) = true . eq loc(s,k) = d . eq l(s,k) <= now(s) = true . -- eq j = k . eq turn(s) = k . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-check(s,k) = true . eq loc(s,k) = d . eq l(s,k) <= now(s) = true . -- eq j = k . eq (turn(s) = k) = false . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-check(s,k) = true . eq loc(s,k) = d . eq l(s,k) <= now(s) = true . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close -- -- 4.2 not c-check(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-check(s,k) = false . -- successor state eq s' = check(s,k) . -- check red istep2(i,j) . close --> 5 exit(s,k) -- 5.1 c-exit(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq loc(s,k) = cs . -- eq i = k . -- successor state eq s' = exit(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq loc(s,k) = cs . -- eq j = k . -- successor state eq s' = exit(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-exit(s,k) = true . eq loc(s,k) = cs . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = exit(s,k) . -- check red istep2(i,j) . close -- -- 5.2 not c-exit(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-exit(s,k) = false . -- successor state eq s' = exit(s,k) . -- check red istep2(i,j) . close --> 6 reset(s,k) -- 6.1 c-reset(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-reset(s,k) = true . eq loc(s,k) = e . -- eq i = k . -- successor state eq s' = reset(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-reset(s,k) = true . eq loc(s,k) = e . -- eq j = k . -- successor state eq s' = reset(s,k) . -- check red istep2(i,j) . close -- open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions -- eq c-reset(s,k) = true . eq loc(s,k) = e . -- eq (i = k) = false . eq (j = k) = false . -- successor state eq s' = reset(s,k) . -- check red istep2(i,j) . close -- -- 6.2 not c-reset(s,k) open ISTEP -- arbitrary objects op k : -> Pid . -- assumptions eq c-reset(s,k) = false . -- successor state eq s' = reset(s,k) . -- check red istep2(i,j) . close --> 7 tick(s,d) -- 7.1 c-tick(s,d) open ISTEP -- arbitrary objects op d : -> Real+ . op k : -> Pid . -- assumptions eq c-tick(s,d) = true . -- successor state eq s' = tick(s,d) . -- check red istep2(i,j) . close -- -- 7.2 not c-tick(s,d) open ISTEP -- arbitrary objects op d : -> Real+ . -- assumptions eq c-tick(s,d) = false . -- successor state eq s' = tick(s,d) . -- check red istep2(i,j) . close --> Q.E.D.