Quelle  slots.thy

(***********************************************************************************
 * 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›
text‹This theory contains the test cases for slots.›

theory slots
imports
  "Shadow_DOM_BaseTest"
begin

definition slots_heap :: "heap_final" where
  "slots_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%20assignments'')),
    (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 18), cast (element_ptr.Ref 19), cast (element_ptr.Ref 21), cast (element_ptr.Ref 22), cast (element_ptr.Ref 30), cast (element_ptr.Ref 31), cast (element_ptr.Ref 39), cast (element_ptr.Ref 40), cast (element_ptr.Ref 48), cast (element_ptr.Ref 49), cast (element_ptr.Ref 57), cast (element_ptr.Ref 58), cast (element_ptr.Ref 64), cast (element_ptr.Ref 65), cast (element_ptr.Ref 71), cast (element_ptr.Ref 72), cast (element_ptr.Ref 78), cast (element_ptr.Ref 79), cast (element_ptr.Ref 85), cast (element_ptr.Ref 86), cast (element_ptr.Ref 92), cast (element_ptr.Ref 93), cast (element_ptr.Ref 112)] fmempty None)),
    (cast (element_ptr.Ref 9), cast (create_element_obj ''div'' [cast (element_ptr.Ref 10)] (fmap_of_list [(''id'', ''test_basic'')]) None)),
    (cast (element_ptr.Ref 10), cast (create_element_obj ''div'' [cast (element_ptr.Ref 11)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 1))))),
    (cast (element_ptr.Ref 11), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 1), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 12)])),
    (cast (element_ptr.Ref 12), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) 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'', ''test_basic_closed'')]) None)),
    (cast (element_ptr.Ref 15), cast (create_element_obj ''div'' [cast (element_ptr.Ref 16)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 2))))),
    (cast (element_ptr.Ref 16), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 2), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 17)])),
    (cast (element_ptr.Ref 17), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 18), 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 19), cast (create_element_obj ''div'' [cast (element_ptr.Ref 20)] (fmap_of_list [(''id'', ''test_slot_not_in_shadow'')]) None)),
    (cast (element_ptr.Ref 20), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1'')]) None)),
    (cast (element_ptr.Ref 21), 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 22), cast (create_element_obj ''div'' [cast (element_ptr.Ref 23), cast (element_ptr.Ref 25)] (fmap_of_list [(''id'', ''test_slot_not_in_shadow_2'')]) None)),
    (cast (element_ptr.Ref 23), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 24)] (fmap_of_list [(''id'', ''s1'')]) None)),
    (cast (element_ptr.Ref 24), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1'')]) None)),
    (cast (element_ptr.Ref 25), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 26), cast (element_ptr.Ref 27)] (fmap_of_list [(''id'', ''s2'')]) None)),
    (cast (element_ptr.Ref 26), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2'')]) None)),
    (cast (element_ptr.Ref 27), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 28), cast (element_ptr.Ref 29)] (fmap_of_list [(''id'', ''s3'')]) None)),
    (cast (element_ptr.Ref 28), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3_1'')]) None)),
    (cast (element_ptr.Ref 29), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3_2'')]) None)),
    (cast (element_ptr.Ref 30), 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 31), cast (create_element_obj ''div'' [cast (element_ptr.Ref 32)] (fmap_of_list [(''id'', ''test_slot_name_matching'')]) None)),
    (cast (element_ptr.Ref 32), cast (create_element_obj ''div'' [cast (element_ptr.Ref 33), cast (element_ptr.Ref 34), cast (element_ptr.Ref 35)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 3))))),
    (cast (element_ptr.Ref 33), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 34), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 35), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''yyy'')]) None)),
    (cast (shadow_root_ptr.Ref 3), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 36), cast (element_ptr.Ref 37), cast (element_ptr.Ref 38)])),
    (cast (element_ptr.Ref 36), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 37), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 38), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3''), (''name'', ''xxx'')]) None)),
    (cast (element_ptr.Ref 39), 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'')),
    (cast (element_ptr.Ref 40), cast (create_element_obj ''div'' [cast (element_ptr.Ref 41)] (fmap_of_list [(''id'', ''test_no_direct_host_child'')]) None)),
    (cast (element_ptr.Ref 41), cast (create_element_obj ''div'' [cast (element_ptr.Ref 42), cast (element_ptr.Ref 43), cast (element_ptr.Ref 44)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 4))))),
    (cast (element_ptr.Ref 42), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 43), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 44), cast (create_element_obj ''div'' [cast (element_ptr.Ref 45)] fmempty None)),
    (cast (element_ptr.Ref 45), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 4), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 46), cast (element_ptr.Ref 47)])),
    (cast (element_ptr.Ref 46), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 47), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 48), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 7)] fmempty None)),
    (cast (character_data_ptr.Ref 7), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 49), cast (create_element_obj ''div'' [cast (element_ptr.Ref 50)] (fmap_of_list [(''id'', ''test_default_slot'')]) None)),
    (cast (element_ptr.Ref 50), cast (create_element_obj ''div'' [cast (element_ptr.Ref 51), cast (element_ptr.Ref 52), cast (element_ptr.Ref 53)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 5))))),
    (cast (element_ptr.Ref 51), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1'')]) None)),
    (cast (element_ptr.Ref 52), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', '''')]) None)),
    (cast (element_ptr.Ref 53), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3''), (''slot'', ''foo'')]) None)),
    (cast (shadow_root_ptr.Ref 5), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 54), cast (element_ptr.Ref 55), cast (element_ptr.Ref 56)])),
    (cast (element_ptr.Ref 54), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 55), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2'')]) None)),
    (cast (element_ptr.Ref 56), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3'')]) None)),
    (cast (element_ptr.Ref 57), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 8)] fmempty None)),
    (cast (character_data_ptr.Ref 8), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 58), cast (create_element_obj ''div'' [cast (element_ptr.Ref 59)] (fmap_of_list [(''id'', ''test_slot_in_slot'')]) None)),
    (cast (element_ptr.Ref 59), cast (create_element_obj ''div'' [cast (element_ptr.Ref 60), cast (element_ptr.Ref 61)] (fmap_of_list [(''id'', ''host'')]) (Some (cast (shadow_root_ptr.Ref 6))))),
    (cast (element_ptr.Ref 60), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 61), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 6), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 62)])),
    (cast (element_ptr.Ref 62), cast (create_element_obj ''slot'' [cast (element_ptr.Ref 63)] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 63), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 64), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 9)] fmempty None)),
    (cast (character_data_ptr.Ref 9), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 65), cast (create_element_obj ''div'' [cast (element_ptr.Ref 66)] (fmap_of_list [(''id'', ''test_slot_is_assigned_to_slot'')]) None)),
    (cast (element_ptr.Ref 66), cast (create_element_obj ''div'' [cast (element_ptr.Ref 67)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 7))))),
    (cast (element_ptr.Ref 67), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 7), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 68)])),
    (cast (element_ptr.Ref 68), cast (create_element_obj ''div'' [cast (element_ptr.Ref 69)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 8))))),
    (cast (element_ptr.Ref 69), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
    (cast (shadow_root_ptr.Ref 8), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 70)])),
    (cast (element_ptr.Ref 70), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 71), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 10)] fmempty None)),
    (cast (character_data_ptr.Ref 10), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 72), cast (create_element_obj ''div'' [cast (element_ptr.Ref 73)] (fmap_of_list [(''id'', ''test_open_closed'')]) None)),
    (cast (element_ptr.Ref 73), cast (create_element_obj ''div'' [cast (element_ptr.Ref 74)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 9))))),
    (cast (element_ptr.Ref 74), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 9), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 75)])),
    (cast (element_ptr.Ref 75), cast (create_element_obj ''div'' [cast (element_ptr.Ref 76)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 10))))),
    (cast (element_ptr.Ref 76), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
    (cast (shadow_root_ptr.Ref 10), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 77)])),
    (cast (element_ptr.Ref 77), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 78), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 11)] fmempty None)),
    (cast (character_data_ptr.Ref 11), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 79), cast (create_element_obj ''div'' [cast (element_ptr.Ref 80)] (fmap_of_list [(''id'', ''test_closed_closed'')]) None)),
    (cast (element_ptr.Ref 80), cast (create_element_obj ''div'' [cast (element_ptr.Ref 81)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 11))))),
    (cast (element_ptr.Ref 81), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 11), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 82)])),
    (cast (element_ptr.Ref 82), cast (create_element_obj ''div'' [cast (element_ptr.Ref 83)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 12))))),
    (cast (element_ptr.Ref 83), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
    (cast (shadow_root_ptr.Ref 12), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 84)])),
    (cast (element_ptr.Ref 84), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 85), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 12)] fmempty None)),
    (cast (character_data_ptr.Ref 12), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 86), cast (create_element_obj ''div'' [cast (element_ptr.Ref 87)] (fmap_of_list [(''id'', ''test_closed_open'')]) None)),
    (cast (element_ptr.Ref 87), cast (create_element_obj ''div'' [cast (element_ptr.Ref 88)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 13))))),
    (cast (element_ptr.Ref 88), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (shadow_root_ptr.Ref 13), cast (create_shadow_root_obj Closed [cast (element_ptr.Ref 89)])),
    (cast (element_ptr.Ref 89), cast (create_element_obj ''div'' [cast (element_ptr.Ref 90)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 14))))),
    (cast (element_ptr.Ref 90), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot2'')]) None)),
    (cast (shadow_root_ptr.Ref 14), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 91)])),
    (cast (element_ptr.Ref 91), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 92), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 13)] fmempty None)),
    (cast (character_data_ptr.Ref 13), cast (create_character_data_obj ''%3C%3Cscript%3E%3E'')),
    (cast (element_ptr.Ref 93), cast (create_element_obj ''div'' [cast (element_ptr.Ref 94)] (fmap_of_list [(''id'', ''test_complex'')]) None)),
    (cast (element_ptr.Ref 94), cast (create_element_obj ''div'' [cast (element_ptr.Ref 95), cast (element_ptr.Ref 96), cast (element_ptr.Ref 97), cast (element_ptr.Ref 98)] (fmap_of_list [(''id'', ''host1'')]) (Some (cast (shadow_root_ptr.Ref 15))))),
    (cast (element_ptr.Ref 95), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c1''), (''slot'', ''slot1'')]) None)),
    (cast (element_ptr.Ref 96), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c2''), (''slot'', ''slot2'')]) None)),
    (cast (element_ptr.Ref 97), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c3'')]) None)),
    (cast (element_ptr.Ref 98), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c4''), (''slot'', ''slot-none'')]) None)),
    (cast (shadow_root_ptr.Ref 15), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 99)])),
    (cast (element_ptr.Ref 99), cast (create_element_obj ''div'' [cast (element_ptr.Ref 100), cast (element_ptr.Ref 101), cast (element_ptr.Ref 102), cast (element_ptr.Ref 103), cast (element_ptr.Ref 104), cast (element_ptr.Ref 105), cast (element_ptr.Ref 106), cast (element_ptr.Ref 107)] (fmap_of_list [(''id'', ''host2'')]) (Some (cast (shadow_root_ptr.Ref 16))))),
    (cast (element_ptr.Ref 100), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s1''), (''name'', ''slot1''), (''slot'', ''slot5'')]) None)),
    (cast (element_ptr.Ref 101), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s2''), (''name'', ''slot2''), (''slot'', ''slot6'')]) None)),
    (cast (element_ptr.Ref 102), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s3'')]) None)),
    (cast (element_ptr.Ref 103), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s4''), (''name'', ''slot4''), (''slot'', ''slot-none'')]) None)),
    (cast (element_ptr.Ref 104), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c5''), (''slot'', ''slot5'')]) None)),
    (cast (element_ptr.Ref 105), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c6''), (''slot'', ''slot6'')]) None)),
    (cast (element_ptr.Ref 106), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c7'')]) None)),
    (cast (element_ptr.Ref 107), cast (create_element_obj ''div'' [] (fmap_of_list [(''id'', ''c8''), (''slot'', ''slot-none'')]) None)),
    (cast (shadow_root_ptr.Ref 16), cast (create_shadow_root_obj Open [cast (element_ptr.Ref 108), cast (element_ptr.Ref 109), cast (element_ptr.Ref 110), cast (element_ptr.Ref 111)])),
    (cast (element_ptr.Ref 108), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s5''), (''name'', ''slot5'')]) None)),
    (cast (element_ptr.Ref 109), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s6''), (''name'', ''slot6'')]) None)),
    (cast (element_ptr.Ref 110), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s7'')]) None)),
    (cast (element_ptr.Ref 111), cast (create_element_obj ''slot'' [] (fmap_of_list [(''id'', ''s8''), (''name'', ''slot8'')]) None)),
    (cast (element_ptr.Ref 112), cast (create_element_obj ''script'' [cast (character_data_ptr.Ref 14)] fmempty None)),
    (cast (character_data_ptr.Ref 14), cast (create_character_data_obj ''%3C%3Cscript%3E%3E''))]"

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


text ‹'Slots: Basic.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_basic'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_basic'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''s1'';
  tmp6 ← tmp5 . assignedNodes();
  tmp7 ← n . ''c1'';
  assert_array_equals(tmp6, [tmp7])
}) slots_heap"
  by eval


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

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_basic'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  tmp3 ← n . ''c1'';
  assert_array_equals(tmp2, [tmp3])
}) slots_heap"
  by eval


text ‹'Slots: Slots in closed.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_basic_closed'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_basic_closed'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None);
  tmp4 ← n . ''s1'';
  tmp5 ← tmp4 . assignedNodes();
  tmp6 ← n . ''c1'';
  assert_array_equals(tmp5, [tmp6])
}) slots_heap"
  by eval


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

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_basic_closed'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  tmp3 ← n . ''c1'';
  assert_array_equals(tmp2, [tmp3])
}) slots_heap"
  by eval


text ‹'Slots: Slots not in a shadow tree.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_slot_not_in_shadow'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_slot_not_in_shadow'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp3 ← tmp2 . assignedNodes();
  assert_array_equals(tmp3, [])
}) slots_heap"
  by eval


text ‹'Slots: Slots not in a shadow tree, elements only.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_slot_not_in_shadow'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''s1'';
  tmp2 ← tmp1 . assignedElements();
  assert_array_equals(tmp2, [])
}) slots_heap"
  by eval


text ‹'Slots: Distributed nodes for Slots not in a shadow tree.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_slot_not_in_shadow_2'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_slot_not_in_shadow_2'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None);
  tmp4 ← n . ''c2'';
  tmp5 ← tmp4 . assignedSlot;
  assert_equals(tmp5, None);
  tmp6 ← n . ''c3_1'';
  tmp7 ← tmp6 . assignedSlot;
  assert_equals(tmp7, None);
  tmp8 ← n . ''c3_2'';
  tmp9 ← tmp8 . assignedSlot;
  assert_equals(tmp9, None);
  tmp10 ← n . ''s1'';
  tmp11 ← tmp10 . assignedNodes();
  assert_array_equals(tmp11, []);
  tmp12 ← n . ''s2'';
  tmp13 ← tmp12 . assignedNodes();
  assert_array_equals(tmp13, []);
  tmp14 ← n . ''s3'';
  tmp15 ← tmp14 . assignedNodes();
  assert_array_equals(tmp15, []);
  tmp16 ← n . ''s1'';
  tmp17 ← tmp16 . assignedNodes(True);
  assert_array_equals(tmp17, []);
  tmp18 ← n . ''s2'';
  tmp19 ← tmp18 . assignedNodes(True);
  assert_array_equals(tmp19, []);
  tmp20 ← n . ''s3'';
  tmp21 ← tmp20 . assignedNodes(True);
  assert_array_equals(tmp21, [])
}) slots_heap"
  by eval


text ‹'Slots: Name matching'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_slot_name_matching'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_slot_name_matching'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''c2'';
  tmp6 ← tmp5 . assignedSlot;
  tmp7 ← n . ''s2'';
  assert_equals(tmp6, tmp7);
  tmp8 ← n . ''c3'';
  tmp9 ← tmp8 . assignedSlot;
  assert_equals(tmp9, None)
}) slots_heap"
  by eval


text ‹'Slots: No direct host child.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_no_direct_host_child'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_no_direct_host_child'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''c2'';
  tmp6 ← tmp5 . assignedSlot;
  tmp7 ← n . ''s1'';
  assert_equals(tmp6, tmp7);
  tmp8 ← n . ''c3'';
  tmp9 ← tmp8 . assignedSlot;
  assert_equals(tmp9, None);
  tmp10 ← n . ''s1'';
  tmp11 ← tmp10 . assignedNodes();
  tmp12 ← n . ''c1'';
  tmp13 ← n . ''c2'';
  assert_array_equals(tmp11, [tmp12, tmp13])
}) slots_heap"
  by eval


text ‹'Slots: Default Slot.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_default_slot'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_default_slot'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s2'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''c2'';
  tmp6 ← tmp5 . assignedSlot;
  tmp7 ← n . ''s2'';
  assert_equals(tmp6, tmp7);
  tmp8 ← n . ''c3'';
  tmp9 ← tmp8 . assignedSlot;
  assert_equals(tmp9, None)
}) slots_heap"
  by eval


text ‹'Slots: Slot in Slot does not matter in assignment.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_slot_in_slot'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_slot_in_slot'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s2'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''c2'';
  tmp6 ← tmp5 . assignedSlot;
  tmp7 ← n . ''s1'';
  assert_equals(tmp6, tmp7)
}) slots_heap"
  by eval


text ‹'Slots: Slot is assigned to another slot'›

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


text ‹'Slots: Open > Closed.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_open_closed'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_open_closed'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''s1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp7 ← n . ''s1'';
  tmp8 ← tmp7 . assignedNodes();
  tmp9 ← n . ''c1'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s2'';
  tmp11 ← tmp10 . assignedNodes();
  tmp12 ← n . ''s1'';
  assert_array_equals(tmp11, [tmp12]);
  tmp13 ← n . ''s1'';
  tmp14 ← tmp13 . assignedNodes(True);
  tmp15 ← n . ''c1'';
  assert_array_equals(tmp14, [tmp15]);
  tmp16 ← n . ''s2'';
  tmp17 ← tmp16 . assignedNodes(True);
  tmp18 ← n . ''c1'';
  assert_array_equals(tmp17, [tmp18])
}) slots_heap"
  by eval


text ‹'Slots: Closed > Closed.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_closed_closed'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_closed_closed'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp4 ← n . ''s1'';
  tmp5 ← tmp4 . assignedSlot;
  assert_equals(tmp5, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp6 ← n . ''s1'';
  tmp7 ← tmp6 . assignedNodes();
  tmp8 ← n . ''c1'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 ← n . ''s2'';
  tmp10 ← tmp9 . assignedNodes();
  tmp11 ← n . ''s1'';
  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_heap"
  by eval


text ‹'Slots: Closed > Open.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_closed_open'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_closed_open'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  assert_equals(tmp3, None, ''A slot in a closed shadow tree should not be accessed via assignedSlot'');
  tmp4 ← n . ''s1'';
  tmp5 ← tmp4 . assignedSlot;
  tmp6 ← n . ''s2'';
  assert_equals(tmp5, tmp6);
  tmp7 ← n . ''s1'';
  tmp8 ← tmp7 . assignedNodes();
  tmp9 ← n . ''c1'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s2'';
  tmp11 ← tmp10 . assignedNodes();
  tmp12 ← n . ''s1'';
  assert_array_equals(tmp11, [tmp12]);
  tmp13 ← n . ''s1'';
  tmp14 ← tmp13 . assignedNodes(True);
  tmp15 ← n . ''c1'';
  assert_array_equals(tmp14, [tmp15]);
  tmp16 ← n . ''s2'';
  tmp17 ← tmp16 . assignedNodes(True);
  tmp18 ← n . ''c1'';
  assert_array_equals(tmp17, [tmp18])
}) slots_heap"
  by eval


text ‹'Slots: Complex case: Basi line.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp3 ← tmp2 . assignedSlot;
  tmp4 ← n . ''s1'';
  assert_equals(tmp3, tmp4);
  tmp5 ← n . ''c2'';
  tmp6 ← tmp5 . assignedSlot;
  tmp7 ← n . ''s2'';
  assert_equals(tmp6, tmp7);
  tmp8 ← n . ''c3'';
  tmp9 ← tmp8 . assignedSlot;
  tmp10 ← n . ''s3'';
  assert_equals(tmp9, tmp10);
  tmp11 ← n . ''c4'';
  tmp12 ← tmp11 . assignedSlot;
  assert_equals(tmp12, None);
  tmp13 ← n . ''s1'';
  tmp14 ← tmp13 . assignedSlot;
  tmp15 ← n . ''s5'';
  assert_equals(tmp14, tmp15);
  tmp16 ← n . ''s2'';
  tmp17 ← tmp16 . assignedSlot;
  tmp18 ← n . ''s6'';
  assert_equals(tmp17, tmp18);
  tmp19 ← n . ''s3'';
  tmp20 ← tmp19 . assignedSlot;
  tmp21 ← n . ''s7'';
  assert_equals(tmp20, tmp21);
  tmp22 ← n . ''s4'';
  tmp23 ← tmp22 . assignedSlot;
  assert_equals(tmp23, None);
  tmp24 ← n . ''c5'';
  tmp25 ← tmp24 . assignedSlot;
  tmp26 ← n . ''s5'';
  assert_equals(tmp25, tmp26);
  tmp27 ← n . ''c6'';
  tmp28 ← tmp27 . assignedSlot;
  tmp29 ← n . ''s6'';
  assert_equals(tmp28, tmp29);
  tmp30 ← n . ''c7'';
  tmp31 ← tmp30 . assignedSlot;
  tmp32 ← n . ''s7'';
  assert_equals(tmp31, tmp32);
  tmp33 ← n . ''c8'';
  tmp34 ← tmp33 . assignedSlot;
  assert_equals(tmp34, None);
  tmp35 ← n . ''s1'';
  tmp36 ← tmp35 . assignedNodes();
  tmp37 ← n . ''c1'';
  assert_array_equals(tmp36, [tmp37]);
  tmp38 ← n . ''s2'';
  tmp39 ← tmp38 . assignedNodes();
  tmp40 ← n . ''c2'';
  assert_array_equals(tmp39, [tmp40]);
  tmp41 ← n . ''s3'';
  tmp42 ← tmp41 . assignedNodes();
  tmp43 ← n . ''c3'';
  assert_array_equals(tmp42, [tmp43]);
  tmp44 ← n . ''s4'';
  tmp45 ← tmp44 . assignedNodes();
  assert_array_equals(tmp45, []);
  tmp46 ← n . ''s5'';
  tmp47 ← tmp46 . assignedNodes();
  tmp48 ← n . ''s1'';
  tmp49 ← n . ''c5'';
  assert_array_equals(tmp47, [tmp48, tmp49]);
  tmp50 ← n . ''s6'';
  tmp51 ← tmp50 . assignedNodes();
  tmp52 ← n . ''s2'';
  tmp53 ← n . ''c6'';
  assert_array_equals(tmp51, [tmp52, tmp53]);
  tmp54 ← n . ''s7'';
  tmp55 ← tmp54 . assignedNodes();
  tmp56 ← n . ''s3'';
  tmp57 ← n . ''c7'';
  assert_array_equals(tmp55, [tmp56, tmp57]);
  tmp58 ← n . ''s8'';
  tmp59 ← tmp58 . assignedNodes();
  assert_array_equals(tmp59, []);
  tmp60 ← n . ''s1'';
  tmp61 ← tmp60 . assignedNodes(True);
  tmp62 ← n . ''c1'';
  assert_array_equals(tmp61, [tmp62]);
  tmp63 ← n . ''s2'';
  tmp64 ← tmp63 . assignedNodes(True);
  tmp65 ← n . ''c2'';
  assert_array_equals(tmp64, [tmp65]);
  tmp66 ← n . ''s3'';
  tmp67 ← tmp66 . assignedNodes(True);
  tmp68 ← n . ''c3'';
  assert_array_equals(tmp67, [tmp68]);
  tmp69 ← n . ''s4'';
  tmp70 ← tmp69 . assignedNodes(True);
  assert_array_equals(tmp70, []);
  tmp71 ← n . ''s5'';
  tmp72 ← tmp71 . assignedNodes(True);
  tmp73 ← n . ''c1'';
  tmp74 ← n . ''c5'';
  assert_array_equals(tmp72, [tmp73, tmp74]);
  tmp75 ← n . ''s6'';
  tmp76 ← tmp75 . assignedNodes(True);
  tmp77 ← n . ''c2'';
  tmp78 ← n . ''c6'';
  assert_array_equals(tmp76, [tmp77, tmp78]);
  tmp79 ← n . ''s7'';
  tmp80 ← tmp79 . assignedNodes(True);
  tmp81 ← n . ''c3'';
  tmp82 ← n . ''c7'';
  assert_array_equals(tmp80, [tmp81, tmp82]);
  tmp83 ← n . ''s8'';
  tmp84 ← tmp83 . assignedNodes(True);
  assert_array_equals(tmp84, [])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: appendChild.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  d1 ← slots_document . createElement(''div'');
  d1 . setAttribute(''slot'', ''slot1'');
  tmp2 ← n . ''host1'';
  tmp2 . appendChild(d1);
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  tmp5 ← n . ''c1'';
  assert_array_equals(tmp4, [tmp5, d1]);
  tmp6 ← d1 . assignedSlot;
  tmp7 ← n . ''s1'';
  assert_equals(tmp6, tmp7);
  tmp8 ← n . ''s5'';
  tmp9 ← tmp8 . assignedNodes(True);
  tmp10 ← n . ''c1'';
  tmp11 ← n . ''c5'';
  assert_array_equals(tmp9, [tmp10, d1, tmp11])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Change slot= attribute 1.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp2 . setAttribute(''slot'', ''slot-none'');
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''c1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None);
  tmp7 ← n . ''s5'';
  tmp8 ← tmp7 . assignedNodes(True);
  tmp9 ← n . ''c5'';
  assert_array_equals(tmp8, [tmp9])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Change slot= attribute 2.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp2 . setAttribute(''slot'', ''slot2'');
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''s2'';
  tmp6 ← tmp5 . assignedNodes();
  tmp7 ← n . ''c1'';
  tmp8 ← n . ''c2'';
  assert_array_equals(tmp6, [tmp7, tmp8]);
  tmp9 ← n . ''c1'';
  tmp10 ← tmp9 . assignedSlot;
  tmp11 ← n . ''s2'';
  assert_equals(tmp10, tmp11);
  tmp12 ← n . ''s5'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c5'';
  assert_array_equals(tmp13, [tmp14]);
  tmp15 ← n . ''s6'';
  tmp16 ← tmp15 . assignedNodes(True);
  tmp17 ← n . ''c1'';
  tmp18 ← n . ''c2'';
  tmp19 ← n . ''c6'';
  assert_array_equals(tmp16, [tmp17, tmp18, tmp19])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Change slot= attribute 3.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c4'';
  tmp2 . setAttribute(''slot'', ''slot1'');
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  tmp5 ← n . ''c1'';
  tmp6 ← n . ''c4'';
  assert_array_equals(tmp4, [tmp5, tmp6]);
  tmp7 ← n . ''c4'';
  tmp8 ← tmp7 . assignedSlot;
  tmp9 ← n . ''s1'';
  assert_equals(tmp8, tmp9);
  tmp10 ← n . ''s5'';
  tmp11 ← tmp10 . assignedNodes(True);
  tmp12 ← n . ''c1'';
  tmp13 ← n . ''c4'';
  tmp14 ← n . ''c5'';
  assert_array_equals(tmp11, [tmp12, tmp13, tmp14])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Remove a child.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''c1'';
  tmp2 . remove();
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''c1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None);
  tmp7 ← n . ''s5'';
  tmp8 ← tmp7 . assignedNodes(True);
  tmp9 ← n . ''c5'';
  assert_array_equals(tmp8, [tmp9])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Add a slot: after.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  slot ← slots_document . createElement(''slot'');
  slot . setAttribute(''name'', ''slot1'');
  tmp2 ← n . ''host2'';
  tmp2 . appendChild(slot);
  tmp3 ← slot . assignedNodes();
  assert_array_equals(tmp3, [])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Add a slot: before.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  slot ← slots_document . createElement(''slot'');
  slot . setAttribute(''name'', ''slot1'');
  tmp3 ← n . ''s1'';
  tmp2 ← n . ''host2'';
  tmp2 . insertBefore(slot, tmp3);
  tmp4 ← slot . assignedNodes();
  tmp5 ← n . ''c1'';
  assert_array_equals(tmp4, [tmp5]);
  tmp6 ← n . ''c1'';
  tmp7 ← tmp6 . assignedSlot;
  assert_equals(tmp7, slot);
  tmp8 ← n . ''s7'';
  tmp9 ← tmp8 . assignedNodes();
  tmp10 ← n . ''s3'';
  tmp11 ← n . ''c7'';
  assert_array_equals(tmp9, [slot, tmp10, tmp11]);
  tmp12 ← n . ''s7'';
  tmp13 ← tmp12 . assignedNodes(True);
  tmp14 ← n . ''c1'';
  tmp15 ← n . ''c3'';
  tmp16 ← n . ''c7'';
  assert_array_equals(tmp13, [tmp14, tmp15, tmp16])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Remove a slot.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp2 . remove();
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  assert_array_equals(tmp4, []);
  tmp5 ← n . ''c1'';
  tmp6 ← tmp5 . assignedSlot;
  assert_equals(tmp6, None);
  tmp7 ← n . ''s5'';
  tmp8 ← tmp7 . assignedNodes();
  tmp9 ← n . ''c5'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 ← n . ''s5'';
  tmp11 ← tmp10 . assignedNodes(True);
  tmp12 ← n . ''c5'';
  assert_array_equals(tmp11, [tmp12])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Change slot name= attribute.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp2 . setAttribute(''name'', ''slot2'');
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  tmp5 ← n . ''c2'';
  assert_array_equals(tmp4, [tmp5]);
  tmp6 ← n . ''c1'';
  tmp7 ← tmp6 . assignedSlot;
  assert_equals(tmp7, None);
  tmp8 ← n . ''c2'';
  tmp9 ← tmp8 . assignedSlot;
  tmp10 ← n . ''s1'';
  assert_equals(tmp9, tmp10);
  tmp11 ← n . ''s5'';
  tmp12 ← tmp11 . assignedNodes();
  tmp13 ← n . ''s1'';
  tmp14 ← n . ''c5'';
  assert_array_equals(tmp12, [tmp13, tmp14]);
  tmp15 ← n . ''s5'';
  tmp16 ← tmp15 . assignedNodes(True);
  tmp17 ← n . ''c2'';
  tmp18 ← n . ''c5'';
  assert_array_equals(tmp16, [tmp17, tmp18])
}) slots_heap"
  by eval


text ‹'Slots: Mutation: Change slot slot= attribute.'›

lemma "test (do {
  tmp0 ← slots_document . getElementById(''test_complex'');
  n ← createTestTree(tmp0);
  tmp1 ← n . ''test_complex'';
  removeWhiteSpaceOnlyTextNodes(tmp1);
  tmp2 ← n . ''s1'';
  tmp2 . setAttribute(''slot'', ''slot6'');
  tmp3 ← n . ''s1'';
  tmp4 ← tmp3 . assignedNodes();
  tmp5 ← n . ''c1'';
  assert_array_equals(tmp4, [tmp5]);
  tmp6 ← n . ''s5'';
  tmp7 ← tmp6 . assignedNodes();
  tmp8 ← n . ''c5'';
  assert_array_equals(tmp7, [tmp8]);
  tmp9 ← n . ''s6'';
  tmp10 ← tmp9 . assignedNodes();
  tmp11 ← n . ''s1'';
  tmp12 ← n . ''s2'';
  tmp13 ← n . ''c6'';
  assert_array_equals(tmp10, [tmp11, tmp12, tmp13]);
  tmp14 ← n . ''s6'';
  tmp15 ← tmp14 . assignedNodes(True);
  tmp16 ← n . ''c1'';
  tmp17 ← n . ''c2'';
  tmp18 ← n . ''c6'';
  assert_array_equals(tmp15, [tmp16, tmp17, tmp18])
}) slots_heap"
  by eval


end