equal
deleted
inserted
replaced
120 apply fastsimp |
120 apply fastsimp |
121 |
121 |
122 apply clarsimp |
122 apply clarsimp |
123 apply (rule_tac x="n'+2" in exI) |
123 apply (rule_tac x="n'+2" in exI) |
124 apply simp |
124 apply simp |
125 apply (drule listE_length)+ |
|
126 apply fastsimp |
|
127 |
125 |
128 apply clarsimp |
126 apply clarsimp |
129 apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI) |
127 apply (rule_tac x="Suc (Suc (Suc (length ST)))" in exI) |
130 apply simp |
128 apply simp |
131 apply (drule listE_length)+ |
|
132 apply fastsimp |
|
133 |
129 |
134 apply clarsimp |
130 apply clarsimp |
135 apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI) |
131 apply (rule_tac x="Suc (Suc (Suc (Suc (length ST))))" in exI) |
136 apply simp |
132 apply simp |
137 apply (drule listE_length)+ |
|
138 apply fastsimp |
|
139 |
133 |
140 apply fastsimp |
134 apply fastsimp |
141 apply fastsimp |
135 apply fastsimp |
142 apply fastsimp |
136 apply fastsimp |
143 apply fastsimp |
137 apply fastsimp |