[STATEMENT]
lemma deleteMin_correct_aux:
  assumes I: "invar q"
  assumes NE: "q\<noteq>[]"
  shows 
  "invar (deleteMin q)"
  "queue_to_multiset_aux (deleteMin q) = queue_to_multiset_aux q - 
  {# (findMin q, eprio (findMin q)) #}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SkewBinomialHeapStruc.invar (map bsmapt (deleteMin q)) &&& SkewBinomialHeapStruc.queue_to_multiset (map bsmapt (deleteMin q)) = SkewBinomialHeapStruc.queue_to_multiset (map bsmapt q) - {#(findMin q, eprio (findMin q))#}
[PROOF STEP]
apply (simp_all add:
    I NE deleteMin_xlate findMin_xlate_aux 
    SkewBinomialHeapStruc.deleteMin_correct)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done