equal
deleted
inserted
replaced
260 where empty = Leaf and isin = isin and insert = insert and delete = delete |
260 where empty = Leaf and isin = isin and insert = insert and delete = delete |
261 and inorder = inorder and inv = rbt |
261 and inorder = inorder and inv = rbt |
262 proof (standard, goal_cases) |
262 proof (standard, goal_cases) |
263 case 1 show ?case by simp |
263 case 1 show ?case by simp |
264 next |
264 next |
265 case 2 thus ?case by(simp add: isin_set) |
265 case 2 thus ?case by(simp add: isin_set_inorder) |
266 next |
266 next |
267 case 3 thus ?case by(simp add: inorder_insert) |
267 case 3 thus ?case by(simp add: inorder_insert) |
268 next |
268 next |
269 case 4 thus ?case by(simp add: inorder_delete) |
269 case 4 thus ?case by(simp add: inorder_delete) |
270 next |
270 next |