equal
deleted
inserted
replaced
122 |
122 |
123 |
123 |
124 Goal "Cli_prg : \ |
124 Goal "Cli_prg : \ |
125 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ |
125 \ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \ |
126 \ Int Invariant giv_meets_ask) \ |
126 \ Int Invariant giv_meets_ask) \ |
127 \ guarantees (LeadsTo {s. k < size (giv s)} \ |
127 \ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})"; |
128 \ {s. k < size (rel s)})"; |
|
129 by (rtac guaranteesI 1); |
128 by (rtac guaranteesI 1); |
130 by (Clarify_tac 1); |
129 by (Clarify_tac 1); |
131 by (rtac Stable_transient_reachable_LeadsTo 1); |
130 by (rtac Stable_transient_reachable_LeadsTo 1); |
132 by (res_inst_tac [("k", "k")] transient_lemma 2); |
131 by (res_inst_tac [("k", "k")] transient_lemma 2); |
133 by (force_tac (claset() addDs [impOfSubs Increasing_size, |
132 by (force_tac (claset() addDs [impOfSubs Increasing_size, |