(***********************************************************************************
 * 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\<open>Testing slots\<close>
text\<open>This theory contains the test cases for slots.\<close>

theory slots
imports
  "Shadow_DOM_BaseTest"
begin

definition slots_heap :: "heap\<^sub>f\<^sub>i\<^sub>n\<^sub>a\<^sub>l" 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 \<open>'Slots: Basic.'\<close>

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


text \<open>'Slots: Basic, elements only.'\<close>

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


text \<open>'Slots: Slots in closed.'\<close>

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


text \<open>'Slots: Slots in closed, elements only.'\<close>

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


text \<open>'Slots: Slots not in a shadow tree.'\<close>

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


text \<open>'Slots: Slots not in a shadow tree, elements only.'\<close>

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


text \<open>'Slots: Distributed nodes for Slots not in a shadow tree.'\<close>

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


text \<open>'Slots: Name matching'\<close>

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


text \<open>'Slots: No direct host child.'\<close>

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


text \<open>'Slots: Default Slot.'\<close>

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


text \<open>'Slots: Slot in Slot does not matter in assignment.'\<close>

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


text \<open>'Slots: Slot is assigned to another slot'\<close>

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


text \<open>'Slots: Open > Closed.'\<close>

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


text \<open>'Slots: Closed > Closed.'\<close>

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"
  by eval


text \<open>'Slots: Closed > Open.'\<close>

lemma "test (do {
  tmp0 \<leftarrow> slots_document . getElementById(''test_closed_open'');
  n \<leftarrow> createTestTree(tmp0);
  tmp1 \<leftarrow> n . ''test_closed_open'';
  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;
  tmp6 \<leftarrow> n . ''s2'';
  assert_equals(tmp5, tmp6);
  tmp7 \<leftarrow> n . ''s1'';
  tmp8 \<leftarrow> tmp7 . assignedNodes();
  tmp9 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp8, [tmp9]);
  tmp10 \<leftarrow> n . ''s2'';
  tmp11 \<leftarrow> tmp10 . assignedNodes();
  tmp12 \<leftarrow> n . ''s1'';
  assert_array_equals(tmp11, [tmp12]);
  tmp13 \<leftarrow> n . ''s1'';
  tmp14 \<leftarrow> tmp13 . assignedNodes(True);
  tmp15 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp14, [tmp15]);
  tmp16 \<leftarrow> n . ''s2'';
  tmp17 \<leftarrow> tmp16 . assignedNodes(True);
  tmp18 \<leftarrow> n . ''c1'';
  assert_array_equals(tmp17, [tmp18])
}) slots_heap"
  by eval


text \<open>'Slots: Complex case: Basi line.'\<close>

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


text \<open>'Slots: Mutation: appendChild.'\<close>

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


text \<open>'Slots: Mutation: Change slot= attribute 1.'\<close>

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


text \<open>'Slots: Mutation: Change slot= attribute 2.'\<close>

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


text \<open>'Slots: Mutation: Change slot= attribute 3.'\<close>

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


text \<open>'Slots: Mutation: Remove a child.'\<close>

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


text \<open>'Slots: Mutation: Add a slot: after.'\<close>

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


text \<open>'Slots: Mutation: Add a slot: before.'\<close>

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


text \<open>'Slots: Mutation: Remove a slot.'\<close>

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


text \<open>'Slots: Mutation: Change slot name= attribute.'\<close>

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


text \<open>'Slots: Mutation: Change slot slot= attribute.'\<close>

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


end