equal
deleted
inserted
replaced
82 apply hypsubst |
82 apply hypsubst |
83 apply (erule exE) |
83 apply (erule exE) |
84 apply (intro strip) |
84 apply (intro strip) |
85 apply (rule_tac p = "b1$ (iterate m$g$x) " in trE) |
85 apply (rule_tac p = "b1$ (iterate m$g$x) " in trE) |
86 prefer 2 apply (assumption) |
86 prefer 2 apply (assumption) |
87 apply (rule le_less_trans [THEN less_irrefl]) |
87 apply (rule le_less_trans [THEN less_irrefl [THEN notE]]) |
88 prefer 2 apply (assumption) |
88 prefer 2 apply (assumption) |
89 apply (rule Least_le) |
89 apply (rule Least_le) |
90 apply (erule hoare_lemma6) |
90 apply (erule hoare_lemma6) |
91 apply (rule le_less_trans [THEN less_irrefl]) |
91 apply (rule le_less_trans [THEN less_irrefl [THEN notE]]) |
92 prefer 2 apply (assumption) |
92 prefer 2 apply (assumption) |
93 apply (rule Least_le) |
93 apply (rule Least_le) |
94 apply (erule hoare_lemma7) |
94 apply (erule hoare_lemma7) |
95 done |
95 done |
96 |
96 |