Theory slots_fallback

(***********************************************************************************
 * Copyright (c) 2016-2020 The University of Sheffield, UK
 *               2019-2020 University of Exeter, UK
 *
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 * * Redistributions of source code must retain the above copyright notice, this
 *   list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright notice,
 *   this list of conditions and the following disclaimer in the documentation
 *   and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
 * FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
 * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
 * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
 * CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
 * OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 ***********************************************************************************)

(* This file is automatically generated, please do not modify! *)

section‹Testing slots\_fallback›
text‹This theory contains the test cases for slots\_fallback.›

theory slots_fallback
imports
  "Shadow_DOM_BaseTest"
begin

definition slots_fallback_heap :: "heap⇩f⇩i⇩n⇩a⇩l" where
  "slots_fallback_heap = create_heap [(cast (document_ptr.Ref 1), cast (create_document_obj html (Some (cast (element_ptr.Ref 1))) [])),
    (cast (element_ptr.Ref 1), cast (create_element_obj ''html'' [cast (element_ptr.Ref 2), cast (element_ptr.Ref 8)] fmempty None)),
    (cast (element_ptr.Ref 2), cast (create_element_obj ''head'' [cast (element_ptr.Ref 3), cast (element_ptr.Ref 4), cast (element_ptr.Ref 5), cast (element_ptr.Ref 6), cast (element_ptr.Ref 7)] fmempty None)),
    (cast (element_ptr.Ref 3), cast (create_element_obj ''title'' [cast (character_data_ptr.Ref 1)] fmempty None)),
    (cast (character_data_ptr.Ref 1), cast (create_character_data_obj ''Shadow%20DOM%3A%20Slots%20and%20fallback%20contents'')),
    (cast (element_ptr.Ref 4), cast (create_element_obj ''meta'' [] (fmap_of_list [(''name'', ''author''), (''title'', ''Hayato Ito''), (''href'', ''mailto:hayato@google.com'')]) None)),
    (cast (element_ptr.Ref 5), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharness.js'')]) None)),
    (cast (element_ptr.Ref 6), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''/resources/testharnessreport.js'')]) None)),
    (cast (element_ptr.Ref 7), cast (create_element_obj ''script'' [] (fmap_of_list [(''src'', ''resources/shadow-dom.js'')]) None)),
    (cast (element_ptr.Ref 8), cast (create_element_obj ''body'' [cast (element_ptr.Ref 9), cast (element_ptr.Ref 13), cast (element_ptr.Ref 14), cast (element_ptr.Ref 19), cast (element_ptr.Ref 20), cast (element_ptr.Ref 26), cast (element_ptr.Ref 27), cast (element_ptr.Ref 33), cast (element_ptr.Ref 34), cast (element_ptr.Ref 46)] fmempty None)),
    (cast (element_ptr.Ref 9), cast (create_element_obj ''div'' [cast (element_ptr.Ref 10)] (fmap_of_list [(''id'', ''test1'')]) None)),
    (cast (element_ptr.Ref 10), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 1))))),
    (cast (shadow_root_ptr.Ref 1), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 11)])),
    (cast (element_ptr.Ref 11), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 12)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 12), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
    (cast (element_ptr.Ref 13), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 2)] fmempty None)),
    (cast (character_data_ptr.Ref 2), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 14), cast (create_element_obj ''div'' [cast (element_ptr.Ref 15)] (fmap_of_list [(''id'', ''test2'')]) None)),
    (cast (element_ptr.Ref 15), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 2))))),
    (cast (shadow_root_ptr.Ref 2), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 16)])),
    (cast (element_ptr.Ref 16), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 17)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 17), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 18)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 18), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
    (cast (element_ptr.Ref 19), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 3)] fmempty None)),
    (cast (character_data_ptr.Ref 3), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 20), cast (create_element_obj ''div'' [cast (element_ptr.Ref 21)] (fmap_of_list [(''id'', ''test3'')]) None)),
    (cast (element_ptr.Ref 21), cast (create_element_obj ''div'' [cast (element_ptr.Ref 22)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 3))))),
    (cast (element_ptr.Ref 22), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 3), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 23)])),
    (cast (element_ptr.Ref 23), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 24)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 24), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 25)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 25), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
    (cast (element_ptr.Ref 26), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 4)] fmempty None)),
    (cast (character_data_ptr.Ref 4), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 27), cast (create_element_obj ''div'' [cast (element_ptr.Ref 28)] (fmap_of_list [(''id'', ''test4'')]) None)),
    (cast (element_ptr.Ref 28), cast (create_element_obj ''div'' [cast (element_ptr.Ref 29)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 4))))),
    (cast (element_ptr.Ref 29), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot2'')]) None)),
    (cast (shadow_root_ptr.Ref 4), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 30)])),
    (cast (element_ptr.Ref 30), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 31)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 31), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 32)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 32), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
    (cast (element_ptr.Ref 33), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 5)] fmempty None)),
    (cast (character_data_ptr.Ref 5), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 34), cast (create_element_obj ''div'' [cast (element_ptr.Ref 35)] (fmap_of_list [(''id'', ''test5'')]) None)),
    (cast (element_ptr.Ref 35), cast (create_element_obj ''div'' [cast (element_ptr.Ref 36)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 5))))),
    (cast (element_ptr.Ref 36), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 5), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 37)])),
    (cast (element_ptr.Ref 37), cast (create_element_obj ''div'' [cast (element_ptr.Ref 38)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 6))))),
    (cast (element_ptr.Ref 38), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 39), cast (element_ptr.Ref 41)] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2''), (''slot'', ''slot3'')]) None)),
    (cast (element_ptr.Ref 39), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 40)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 40), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f1'')]) None)),
    (cast (element_ptr.Ref 41), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f2'')]) None)),
    (cast (shadow_root_ptr.Ref 6), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 42)])),
    (cast (element_ptr.Ref 42), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 43), cast (element_ptr.Ref 45)] (fmap_of_list [(''id'', ''s4''), (''name'', ''slot4'')]) None)),
    (cast (element_ptr.Ref 43), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 44)] (fmap_of_list [(''id'', ''s3''), (''name'', ''slot3'')]) None)),
    (cast (element_ptr.Ref 44), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f3'')]) None)),
    (cast (element_ptr.Ref 45), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''f4'')]) None)),
    (cast (element_ptr.Ref 46), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 6)] fmempty None)),
    (cast (character_data_ptr.Ref 6), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"

definition slots_fallback_document :: "(unit, unit, unit, unit, unit, unit) object_ptr option" where "slots_fallback_document = Some (cast (document_ptr.Ref 1))"


text ‹'Slots fallback: Basic.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test1'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test1'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''f1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None);
  tmp4 ← n . ''s1'';
  tmp5 ← tmp4 . assignedNodes();
  assert_array_equals(tmp5, []);
  tmp6 ← n . ''s1'';
  tmp7 ← tmp6 . assignedNodes(True);
  tmp8 ← n . ''f1'';
  assert_array_equals(tmp7, [tmp8])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Basic, elements only.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test1'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  assert_array_equals(tmp2, []);
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedElements(True);
  tmp5 ← n . ''f1'';
  assert_array_equals(tmp4, [tmp5])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Slots in Slots.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test2'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test2'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''f1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None);
  tmp4 ← n . ''s1'';
  tmp5 ← tmp4 . assignedNodes();
  assert_array_equals(tmp5, []);
  tmp6 ← n . ''s2'';
  tmp7 ← tmp6 . assignedNodes();
  assert_array_equals(tmp7, []);
  tmp8 ← n . ''s1'';
  tmp9 ← tmp8 . assignedNodes(True);
  tmp10 ← n . ''f1'';
  assert_array_equals(tmp9, [tmp10]);
  tmp11 ← n . ''s2'';
  tmp12 ← tmp11 . assignedNodes(True);
  tmp13 ← n . ''f1'';
  assert_array_equals(tmp12, [tmp13])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Slots in Slots, elements only.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test2'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  assert_array_equals(tmp2, []);
  tmp3 ← n . ''s2'';
  tmp4 ← tmp3 . assignedElements();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''s1'';
  tmp6 ← tmp5 . assignedElements(True);
  tmp7 ← n . ''f1'';
  assert_array_equals(tmp6, [tmp7]);
  tmp8 ← n . ''s2'';
  tmp9 ← tmp8 . assignedElements(True);
  tmp10 ← n . ''f1'';
  assert_array_equals(tmp9, [tmp10])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Fallback contents should not be used if a node is assigned.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test3'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test3'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''f1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None);
  tmp7 ← n . ''s1'';
  tmp8 ← tmp7 . assignedNodes();
  tmp9 ← n . ''c1'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s2'';
  tmp11 ← tmp10 . assignedNodes();
  assert_array_equals(tmp11, []);
  tmp12 ← n . ''s1'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c1'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 ← n . ''s2'';
  tmp16 ← tmp15 . assignedNodes(True);
  tmp17 ← n . ''f1'';
  assert_array_equals(tmp16, [tmp17])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Slots in Slots: Assigned nodes should be used as fallback contents of another slot'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test4'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test4'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s2'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''f1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None);
  tmp7 ← n . ''s1'';
  tmp8 ← tmp7 . assignedNodes();
  assert_array_equals(tmp8, []);
  tmp9 ← n . ''s2'';
  tmp10 ← tmp9 . assignedNodes();
  tmp11 ← n . ''c1'';
  assert_array_equals(tmp10, [tmp11]);
  tmp12 ← n . ''s1'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c1'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 ← n . ''s2'';
  tmp16 ← tmp15 . assignedNodes(True);
  tmp17 ← n . ''c1'';
  assert_array_equals(tmp16, [tmp17])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Complex case.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp3 ← tmp2 . assignedNodes();
  tmp4 ← n . ''c1'';
  assert_array_equals(tmp3, [tmp4]);
  tmp5 ← n . ''s2'';
  tmp6 ← tmp5 . assignedNodes();
  assert_array_equals(tmp6, []);
  tmp7 ← n . ''s3'';
  tmp8 ← tmp7 . assignedNodes();
  tmp9 ← n . ''s2'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s4'';
  tmp11 ← tmp10 . assignedNodes();
  assert_array_equals(tmp11, []);
  tmp12 ← n . ''s1'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c1'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 ← n . ''s2'';
  tmp16 ← tmp15 . assignedNodes(True);
  tmp17 ← n . ''c1'';
  tmp18 ← n . ''f2'';
  assert_array_equals(tmp16, [tmp17, tmp18]);
  tmp19 ← n . ''s3'';
  tmp20 ← tmp19 . assignedNodes(True);
  tmp21 ← n . ''c1'';
  tmp22 ← n . ''f2'';
  assert_array_equals(tmp20, [tmp21, tmp22]);
  tmp23 ← n . ''s4'';
  tmp24 ← tmp23 . assignedNodes(True);
  tmp25 ← n . ''c1'';
  tmp26 ← n . ''f2'';
  tmp27 ← n . ''f4'';
  assert_array_equals(tmp24, [tmp25, tmp26, tmp27])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Complex case, elements only.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  tmp3 ← n . ''c1'';
  assert_array_equals(tmp2, [tmp3]);
  tmp4 ← n . ''s2'';
  tmp5 ← tmp4 . assignedElements();
  assert_array_equals(tmp5, []);
  tmp6 ← n . ''s3'';
  tmp7 ← tmp6 . assignedElements();
  tmp8 ← n . ''s2'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 ← n . ''s4'';
  tmp10 ← tmp9 . assignedElements();
  assert_array_equals(tmp10, []);
  tmp11 ← n . ''s1'';
  tmp12 ← tmp11 . assignedElements(True);
  tmp13 ← n . ''c1'';
  assert_array_equals(tmp12, [tmp13]);
  tmp14 ← n . ''s2'';
  tmp15 ← tmp14 . assignedElements(True);
  tmp16 ← n . ''c1'';
  tmp17 ← n . ''f2'';
  assert_array_equals(tmp15, [tmp16, tmp17]);
  tmp18 ← n . ''s3'';
  tmp19 ← tmp18 . assignedElements(True);
  tmp20 ← n . ''c1'';
  tmp21 ← n . ''f2'';
  assert_array_equals(tmp19, [tmp20, tmp21]);
  tmp22 ← n . ''s4'';
  tmp23 ← tmp22 . assignedElements(True);
  tmp24 ← n . ''c1'';
  tmp25 ← n . ''f2'';
  tmp26 ← n . ''f4'';
  assert_array_equals(tmp23, [tmp24, tmp25, tmp26])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Mutation. Append fallback contents.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  d1 ← slots_fallback_document . createElement(''div'');
  tmp2 ← n . ''s2'';
  tmp2 . appendChild(d1);
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes(True);
  tmp5 ← n . ''c1'';
  assert_array_equals(tmp4, [tmp5]);
  tmp6 ← n . ''s2'';
  tmp7 ← tmp6 . assignedNodes(True);
  tmp8 ← n . ''c1'';
  tmp9 ← n . ''f2'';
  assert_array_equals(tmp7, [tmp8, tmp9, d1]);
  tmp10 ← n . ''s3'';
  tmp11 ← tmp10 . assignedNodes(True);
  tmp12 ← n . ''c1'';
  tmp13 ← n . ''f2'';
  assert_array_equals(tmp11, [tmp12, tmp13, d1]);
  tmp14 ← n . ''s4'';
  tmp15 ← tmp14 . assignedNodes(True);
  tmp16 ← n . ''c1'';
  tmp17 ← n . ''f2'';
  tmp18 ← n . ''f4'';
  assert_array_equals(tmp15, [tmp16, tmp17, d1, tmp18])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Mutation. Remove fallback contents.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''f2'';
  tmp2 . remove();
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes(True);
  tmp5 ← n . ''c1'';
  assert_array_equals(tmp4, [tmp5]);
  tmp6 ← n . ''s2'';
  tmp7 ← tmp6 . assignedNodes(True);
  tmp8 ← n . ''c1'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 ← n . ''s3'';
  tmp10 ← tmp9 . assignedNodes(True);
  tmp11 ← n . ''c1'';
  assert_array_equals(tmp10, [tmp11]);
  tmp12 ← n . ''s4'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c1'';
  tmp15 ← n . ''f4'';
  assert_array_equals(tmp13, [tmp14, tmp15])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Mutation. Assign a node to a slot so that fallback contens are no longer used.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  d2 ← slots_fallback_document . createElement(''div'');
  d2 . setAttribute(''slot'', ''slot2'');
  tmp2 ← n . ''host1'';
  tmp2 . appendChild(d2);
  tmp3 ← n . ''s2'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, [d2]);
  tmp5 ← n . ''s2'';
  tmp6 ← tmp5 . assignedNodes(True);
  assert_array_equals(tmp6, [d2]);
  tmp7 ← n . ''s3'';
  tmp8 ← tmp7 . assignedNodes(True);
  assert_array_equals(tmp8, [d2]);
  tmp9 ← n . ''s4'';
  tmp10 ← tmp9 . assignedNodes(True);
  tmp11 ← n . ''f4'';
  assert_array_equals(tmp10, [d2, tmp11])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Mutation. Remove an assigned node from a slot so that fallback contens will be used.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp2 . remove();
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''s1'';
  tmp6 ← tmp5 . assignedNodes(True);
  tmp7 ← n . ''f1'';
  assert_array_equals(tmp6, [tmp7]);
  tmp8 ← n . ''s2'';
  tmp9 ← tmp8 . assignedNodes(True);
  tmp10 ← n . ''f1'';
  tmp11 ← n . ''f2'';
  assert_array_equals(tmp9, [tmp10, tmp11]);
  tmp12 ← n . ''s3'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''f1'';
  tmp15 ← n . ''f2'';
  assert_array_equals(tmp13, [tmp14, tmp15]);
  tmp16 ← n . ''s4'';
  tmp17 ← tmp16 . assignedNodes(True);
  tmp18 ← n . ''f1'';
  tmp19 ← n . ''f2'';
  tmp20 ← n . ''f4'';
  assert_array_equals(tmp17, [tmp18, tmp19, tmp20])
}) slots_fallback_heap"
  by eval


text ‹'Slots fallback: Mutation.  Remove a slot which is a fallback content of another slot.'›

lemma "test (do {
  tmp0 ← slots_fallback_document . getElementById(''test5'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test5'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp2 . remove();
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''s1'';
  tmp6 ← tmp5 . assignedNodes(True);
  assert_array_equals(tmp6, [], ''fall back contents should be empty because s1 is not in a shadow tree.'');
  tmp7 ← n . ''s2'';
  tmp8 ← tmp7 . assignedNodes(True);
  tmp9 ← n . ''f2'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s3'';
  tmp11 ← tmp10 . assignedNodes(True);
  tmp12 ← n . ''f2'';
  assert_array_equals(tmp11, [tmp12]);
  tmp13 ← n . ''s4'';
  tmp14 ← tmp13 . assignedNodes(True);
  tmp15 ← n . ''f2'';
  tmp16 ← n . ''f4'';
  assert_array_equals(tmp14, [tmp15, tmp16])
}) slots_fallback_heap"
  by eval


end