[STATEMENT]
lemma "test (do {
  tmp0 \<leftarrow> slots_document . getElementById(''test_closed_closed'');
  n \<leftarrow> createTestTree(tmp0);
  tmp1 \<leftarrow> n . ''test_closed_closed'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 \<leftarrow> n . ''c1'';
  tmp3 \<leftarrow> tmp2 . assignedSlot;
  assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp4 \<leftarrow> n . ''s1'';
  tmp5 \<leftarrow> tmp4 . assignedSlot;
  assert_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp6 \<leftarrow> n . ''s1'';
  tmp7 \<leftarrow> tmp6 . assignedNodes();
  tmp8 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 \<leftarrow> n . ''s2'';
  tmp10 \<leftarrow> tmp9 . assignedNodes();
  tmp11 \<leftarrow> n . ''s1'';
  assert_array_equals(tmp10, [tmp11]);
  tmp12 \<leftarrow> n . ''s1'';
  tmp13 \<leftarrow> tmp12 . assignedNodes(True);
  tmp14 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 \<leftarrow> n . ''s2'';
  tmp16 \<leftarrow> tmp15 . assignedNodes(True);
  tmp17 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp16, [tmp17])
}) slots_heap"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. test (Heap_Error_Monad.bind slots_document . getElementById(''test_closed_closed'') (\<lambda>tmp0. Heap_Error_Monad.bind (createTestTree tmp0) (\<lambda>n. Heap_Error_Monad.bind (n . ''test_closed_closed'') (\<lambda>tmp1. Heap_Error_Monad.bind (removeWhiteSpaceOnlyTextNodes tmp1) (\<lambda>_. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp2. Heap_Error_Monad.bind tmp2 . assignedSlot (\<lambda>tmp3. Heap_Error_Monad.bind assert_array_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'') (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp4. Heap_Error_Monad.bind tmp4 . assignedSlot (\<lambda>tmp5. Heap_Error_Monad.bind assert_array_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'') (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp6. Heap_Error_Monad.bind tmp6 . assignedNodes() (\<lambda>tmp7. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp8. Heap_Error_Monad.bind assert_array_equals(tmp7, [tmp8]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s2'') (\<lambda>tmp9. Heap_Error_Monad.bind tmp9 . assignedNodes() (\<lambda>tmp10. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp11. Heap_Error_Monad.bind assert_array_equals(tmp10, [tmp11]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s1'') (\<lambda>tmp12. Heap_Error_Monad.bind tmp12 . assignedNodes(True) (\<lambda>tmp13. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp14. Heap_Error_Monad.bind assert_array_equals(tmp13, [tmp14]) (\<lambda>_. Heap_Error_Monad.bind (n . ''s2'') (\<lambda>tmp15. Heap_Error_Monad.bind tmp15 . assignedNodes(True) (\<lambda>tmp16. Heap_Error_Monad.bind (n . ''c1'') (\<lambda>tmp17. assert_array_equals(tmp16, [tmp17]))))))))))))))))))))))))))) slots_heap
[PROOF STEP]
by eval