\x t -> insert x t

===[unfold + simplification                      (step 1)

\x t -> 
    some
     (\s -> 
        heapinv t && 
        heapinv s && 
        equals (nonemptybag x (abstraction t))
         (abstraction s)
     )

===[unfold + simplification                      (step 2)

\x t -> 
    some
     (\s -> 
        heapinv t && 
        heapinv s && 
        equals
         (nonemptybag x
           (case t of
              Leaf -> emptybag
              Node l e r -> 
               unionbag
                (unionbag (abstraction l) (singletonbag e))
                (abstraction r)
           )
         )
         (abstraction s)
     )

===[tactic simplify                              (step 3)

\x t -> 
    case t of
      Leaf -> 
       some
        (\s -> 
           heapinv Leaf && 
           heapinv s && 
           equals (nonemptybag x emptybag) (abstraction s)
        )
      Node l e r -> 
       some
        (\s -> 
           heapinv (Node l e r) && 
           heapinv s && 
           equals
            (nonemptybag x
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (abstraction r)
              )
            )
            (abstraction s)
        )

===[tactic solve                                 (step 4)

\x t -> 
    case t of
      Leaf -> 
       some
        (\s -> 
           heapinv s && 
           equals (nonemptybag x emptybag) (abstraction s)
        )
      Node l e r -> 
       some
        (\s -> 
           heapinv (Node l e r) && 
           heapinv s && 
           equals
            (nonemptybag x
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (abstraction r)
              )
            )
            (abstraction s)
        )

===[apply rule tree-derived.thy/some_heap_equals_nonempty_abstr (step 5)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       some
        (\s -> 
           heapinv (Node l e r) && 
           heapinv s && 
           equals
            (nonemptybag x
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (abstraction r)
              )
            )
            (abstraction s)
        )

===[apply rule general.thy/commutativity         (step 6)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       some
        (\s -> 
           heapinv (Node l e r) && 
           heapinv s && 
           equals (abstraction s)
            (nonemptybag x
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (abstraction r)
              )
            )
        )

===[apply rule bag-derived.thy/union_union_single backwards (step 7)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       some
        (\s -> 
           heapinv (Node l e r) && 
           heapinv s && 
           equals (abstraction s)
            (unionbag
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (singletonbag x)
              )
              (abstraction r)
            )
        )

===[apply rule tree-added.thy/heap_insert + simplification (step 8)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       some
        (\s -> 
           (if e <= x 
            then heapinv (Node l e r) && 
                 heapinv (Node (insert x r) e l) 
            else heapinv (Node l e r) && 
                 heapinv (Node (insert e r) x l)
           ) && 
           heapinv s && 
           equals (abstraction s)
            (unionbag
              (unionbag
                (unionbag (abstraction l) (singletonbag e))
                (singletonbag x)
              )
              (abstraction r)
            )
        )

===[tactic simplify                              (step 9)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       if e <= x 
       then some
             (\s -> 
                (heapinv (Node l e r) && 
                 heapinv (Node (insert x r) e l)
                ) && 
                heapinv s && 
                equals (abstraction s)
                 (unionbag
                   (unionbag
                     (unionbag (abstraction l)
                       (singletonbag e)
                     )
                     (singletonbag x)
                   )
                   (abstraction r)
                 )
             ) 
       else some
             (\s -> 
                (heapinv (Node l e r) && 
                 heapinv (Node (insert e r) x l)
                ) && 
                heapinv s && 
                equals (abstraction s)
                 (unionbag
                   (unionbag
                     (unionbag (abstraction l)
                       (singletonbag e)
                     )
                     (singletonbag x)
                   )
                   (abstraction r)
                 )
             )

=>=[apply rule tree-derived.thy/some_heap_insert_1 (step 10)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       if e <= x 
       then Node (insert x r) e l 
       else some
             (\s -> 
                (heapinv (Node l e r) && 
                 heapinv (Node (insert e r) x l)
                ) && 
                heapinv s && 
                equals (abstraction s)
                 (unionbag
                   (unionbag
                     (unionbag (abstraction l)
                       (singletonbag e)
                     )
                     (singletonbag x)
                   )
                   (abstraction r)
                 )
             )

=>=[apply rule tree-derived.thy/some_heap_insert_2 (step 11)

\x t -> 
    case t of
      Leaf -> Node Leaf x Leaf
      Node l e r -> 
       if e <= x 
       then Node (insert x r) e l 
       else Node (insert e r) x l