From 8fa45ccb0d21b389587fb02909762ecf6cb721d6 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 17 Apr 2024 16:27:09 -0500 Subject: [PATCH] Store base pointer offset for map/list/set children of blocks and use this to migrate during garbage collection with -O3 (#1026) Previously there existed a bug that would occur if the following happened: 1. A garbage collection is triggered with at least two roots: a. A map/list/set which is a child of a symbol-layout block b. A symbol-layout block that recursively points to the symbol-layout block which is the parent of the map/list/set 2. Garbage collection does not copy the symbol which is the parent of the map/list/set when tackling root 1a above. It merely tackles the internal memory allocated by that map/list/set. 3. Garbage collection moves the block to the new allocation semispace. The root pointer to the map/list/set still points to the collection semispace. 4. Garbage collection ends, leaking a pointer into the collection semispace. This memory has been corrupted by storing forwarding pointers to the allocation semispace. 5. The backend tries to read the map/list/set, but its length field is corrupted by the forwarding pointer, leading to a segfault. In order to fix this, we annotate each map/list/set child of a block with a "base pointer offset". This offset is an integer that, when added to the address of the map/list/set pointer which is 8 bytes following it, will return the address of the block header of the containing block. We do not try to modify `get_value_type` since that would be very intrusive as a change; instead we only modify the logic which selects children of blocks using llvm `getelementptr` instructions, as well as the code that creates map/list/set children in blocks in the first place. Once these annotations have been applied, which is the subject of the first 5 commits in this PR, we modify the garbage collector to use them in order to reconstruct the base pointer when it receives a garbage collection root. We refactor out a `migrate_root` function which handles GC roots, and rename `migrate_roots` to `migrate_static_roots` to avoid confusion. Then we modify `migrate_root` to reconstruct the base pointer, migrate the base pointer, and then write the updated derived pointer back to the array of gc roots. We no longer need to call `migrate_map`, `migrate_set`, or `migrate_list` on the resulting map/list/set because this will now occur for us during evacuation of the relevant parent block. Code to handle the case where a map/list/set pointer is bare on the alwaysgcspace rather than a child of a block remains largely unchanged, except that we need to modify how we convert those collection to the kore heap in order to accommodate the new memory layout. Finally, we add a test. I ran the test on the master branch of K and it failed. --- include/kllvm/codegen/CreateTerm.h | 2 + include/kllvm/codegen/Util.h | 3 + include/runtime/collect.h | 2 + lib/codegen/CreateStaticTerm.cpp | 12 +- lib/codegen/CreateTerm.cpp | 43 +- lib/codegen/Decision.cpp | 7 +- lib/codegen/EmitConfigParser.cpp | 27 +- lib/codegen/Util.cpp | 14 + runtime/collect/CMakeLists.txt | 2 +- runtime/collect/collect.cpp | 85 +- ...ate_roots.cpp => migrate_static_roots.cpp} | 4 +- test/defn/k-files/migrate-map-root.k | 14 + test/defn/migrate-map-root.kore | 2469 +++++++++++++++++ test/input/migrate-map-root.in | 1 + test/output/migrate-map-root.out.diff | 1 + 15 files changed, 2630 insertions(+), 56 deletions(-) rename runtime/collect/{migrate_roots.cpp => migrate_static_roots.cpp} (94%) create mode 100644 test/defn/k-files/migrate-map-root.k create mode 100644 test/defn/migrate-map-root.kore create mode 100644 test/input/migrate-map-root.in create mode 100644 test/output/migrate-map-root.out.diff diff --git a/include/kllvm/codegen/CreateTerm.h b/include/kllvm/codegen/CreateTerm.h index bbe5bd00a..ed54db584 100644 --- a/include/kllvm/codegen/CreateTerm.h +++ b/include/kllvm/codegen/CreateTerm.h @@ -89,6 +89,8 @@ new_module(std::string const &name, llvm::LLVMContext &context); llvm::StructType *get_block_type( llvm::Module *module, kore_definition *definition, kore_symbol const *symbol); +uint64_t get_block_offset( + kore_definition *definition, kore_symbol const *symbol, int idx); uint64_t get_block_header_val( llvm::Module *module, kore_symbol const *symbol, llvm::Type *block_type); llvm::Value *get_block_header( diff --git a/include/kllvm/codegen/Util.h b/include/kllvm/codegen/Util.h index 2834c0e92..c64236999 100644 --- a/include/kllvm/codegen/Util.h +++ b/include/kllvm/codegen/Util.h @@ -2,6 +2,7 @@ #define KLLVM_UTIL_H #include +#include #include #include #include @@ -11,6 +12,8 @@ namespace kllvm { +llvm::Constant *get_offset_of_member(llvm::Module *, llvm::StructType *, int); + // Returns a reference to the function declaration for a memory allocation // function with the given name, adding a declaration to the current module if // one does not yet exist diff --git a/include/runtime/collect.h b/include/runtime/collect.h index bdbbcd476..7ced6aa27 100644 --- a/include/runtime/collect.h +++ b/include/runtime/collect.h @@ -29,6 +29,8 @@ extern "C" { extern size_t numBytesLiveAtCollection[1 << AGE_WIDTH]; extern bool collect_old; size_t get_size(uint64_t, uint16_t); +void migrate_static_roots(void); +void migrate(block **block_ptr); void migrate_once(block **); void migrate_list(void *l); void migrate_map(void *m); diff --git a/lib/codegen/CreateStaticTerm.cpp b/lib/codegen/CreateStaticTerm.cpp index 8e224bf47..6b769bd5d 100644 --- a/lib/codegen/CreateStaticTerm.cpp +++ b/lib/codegen/CreateStaticTerm.cpp @@ -58,10 +58,18 @@ llvm::Constant *create_static_term::not_injection_case( block_vals.push_back(llvm::ConstantArray::get( empty_array_type, llvm::ArrayRef())); - int idx = 2; + int idx = 0; for (auto const &child : constructor->get_arguments()) { + auto *sort = dynamic_cast( + symbol->get_arguments()[idx].get()); + auto cat = sort->get_category(definition_); + if (is_collection_sort(cat)) { + block_vals.push_back(get_offset_of_member( + module_, block_header_type, + get_block_offset(definition_, symbol, idx))); + } llvm::Constant *child_value = nullptr; - if (idx++ == 2 && val != nullptr) { + if (idx++ == 0 && val != nullptr) { child_value = val; } else { child_value = (*this)(child.get()).first; diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp index 1f6f09a8c..9a1f32d4e 100644 --- a/lib/codegen/CreateTerm.cpp +++ b/lib/codegen/CreateTerm.cpp @@ -200,12 +200,39 @@ llvm::StructType *get_block_type( types.push_back(empty_array_type); for (auto const &arg : symbol->get_arguments()) { auto *sort = dynamic_cast(arg.get()); + auto cat = sort->get_category(definition); + if (is_collection_sort(cat)) { + types.push_back(llvm::Type::getInt64Ty(module->getContext())); + } llvm::Type *type = getvalue_type(sort->get_category(definition), module); types.push_back(type); } return llvm::StructType::get(module->getContext(), types); } +uint64_t get_block_offset( + kore_definition *definition, kore_symbol const *symbol, int idx) { + uint64_t result = 2; + int i = 0; + for (auto const &arg : symbol->get_arguments()) { + auto *sort = dynamic_cast(arg.get()); + auto cat = sort->get_category(definition); + if (is_collection_sort(cat)) { + if (i == idx) { + return result + 1; + } + result += 2; + } else { + if (i == idx) { + return result; + } + result += 1; + } + i++; + } + throw std::invalid_argument("idx not within bounds of symbol"); +} + uint64_t get_block_header_val( llvm::Module *module, kore_symbol const *symbol, llvm::Type *block_type) { uint64_t header_val = symbol->get_tag(); @@ -779,24 +806,30 @@ llvm::Value *create_term::not_injection_case( llvm::StructType *block_type = get_block_type(module_, definition_, symbol); llvm::Value *block_header = get_block_header(module_, definition_, symbol, block_type); - int idx = 2; + int idx = 0; std::vector children; for (auto const &child : constructor->get_arguments()) { + auto *sort = dynamic_cast(child->get_sort().get()); + auto cat = sort->get_category(definition_); + if (is_collection_sort(cat)) { + children.push_back(get_offset_of_member( + module_, block_type, get_block_offset(definition_, symbol, idx))); + } llvm::Value *child_value = nullptr; - if (idx == 2 && val != nullptr) { + if (idx == 0 && val != nullptr) { child_value = val; } else { - std::string new_location = fmt::format("{}:{}", location_stack, idx - 2); + std::string new_location = fmt::format("{}:{}", location_stack, idx); if (is_injection_symbol(child.get(), definition_->get_inj_symbol())) { new_location = location_stack; } child_value = create_allocation(child.get(), new_location).first; } - auto *sort = dynamic_cast(child->get_sort().get()); if (sort && is_collection_sort(sort->get_category(definition_))) { child_value = new llvm::LoadInst( - block_type->elements()[idx], child_value, "", current_block_); + block_type->elements()[get_block_offset(definition_, symbol, idx)], + child_value, "", current_block_); } children.push_back(child_value); idx++; diff --git a/lib/codegen/Decision.cpp b/lib/codegen/Decision.cpp index cd22abfd0..4c2b53dc1 100644 --- a/lib/codegen/Decision.cpp +++ b/lib/codegen/Decision.cpp @@ -246,7 +246,9 @@ void switch_node::codegen(decision *d) { block_type, cast, {llvm::ConstantInt::get(llvm::Type::getInt64Ty(d->ctx_), 0), llvm::ConstantInt::get( - llvm::Type::getInt32Ty(d->ctx_), offset + 2)}, + llvm::Type::getInt32Ty(d->ctx_), + get_block_offset( + d->definition_, switch_case.get_constructor(), offset))}, "", d->current_block_); llvm::Value *child = nullptr; @@ -851,7 +853,8 @@ void abort_when_stuck( llvm::Value *child_ptr = llvm::GetElementPtrInst::CreateInBounds( block_type, block, {llvm::ConstantInt::get(llvm::Type::getInt64Ty(ctx), 0), - llvm::ConstantInt::get(llvm::Type::getInt32Ty(ctx), idx + 2)}, + llvm::ConstantInt::get( + llvm::Type::getInt32Ty(ctx), get_block_offset(d, symbol, idx))}, "", current_block); if (is_collection_sort(cat)) { child_value = new llvm::LoadInst( diff --git a/lib/codegen/EmitConfigParser.cpp b/lib/codegen/EmitConfigParser.cpp index aff00accd..623c31fa4 100644 --- a/lib/codegen/EmitConfigParser.cpp +++ b/lib/codegen/EmitConfigParser.cpp @@ -859,7 +859,9 @@ static void get_store( llvm::Type *arg_ty = get_arg_type(cat, module); llvm::Value *child_ptr = llvm::GetElementPtrInst::CreateInBounds( block_type, cast, - {zero, llvm::ConstantInt::get(llvm::Type::getInt32Ty(ctx), idx++ + 2)}, + {zero, llvm::ConstantInt::get( + llvm::Type::getInt32Ty(ctx), + get_block_offset(definition, symbol, idx++))}, "", case_block); if (is_collection_sort(cat)) { arg = new llvm::LoadInst(arg_ty, arg, "", case_block); @@ -954,7 +956,9 @@ static void get_visitor( value_type cat = composite_sort->get_category(definition); llvm::Value *child_ptr = llvm::GetElementPtrInst::CreateInBounds( block_type, cast, - {zero, llvm::ConstantInt::get(llvm::Type::getInt32Ty(ctx), idx++ + 2)}, + {zero, llvm::ConstantInt::get( + llvm::Type::getInt32Ty(ctx), + get_block_offset(definition, symbol, idx++))}, "", case_block); llvm::Value *child = new llvm::LoadInst( getvalue_type(cat, module), child_ptr, "", case_block); @@ -1114,20 +1118,6 @@ static void get_visitor( } } -static llvm::Constant *get_offset_of_member( - [[maybe_unused]] llvm::Module *mod, llvm::StructType *struct_ty, - int nth_member) { -#if LLVM_VERSION_MAJOR >= 17 - auto offset - = llvm::DataLayout(mod).getStructLayout(struct_ty)->getElementOffset( - nth_member); - auto *offset_ty = llvm::Type::getInt64Ty(mod->getContext()); - return llvm::ConstantInt::get(offset_ty, offset); -#else - return llvm::ConstantExpr::getOffsetOf(struct_ty, nth_member); -#endif -} - static llvm::Constant *get_layout_data( uint16_t layout, kore_symbol *symbol, llvm::Module *module, kore_definition *def) { @@ -1135,13 +1125,12 @@ static llvm::Constant *get_layout_data( std::vector elements; llvm::LLVMContext &ctx = module->getContext(); auto *block_type = get_block_type(module, def, symbol); - int i = 2; + int i = 0; for (auto const &sort : symbol->get_arguments()) { value_type cat = dynamic_cast(sort.get())->get_category(def); auto *offset = get_offset_of_member( - module, block_type, - i++); //llvm::ConstantExpr::getOffsetOf(BlockType, i++); + module, block_type, get_block_offset(def, symbol, i++)); elements.push_back(llvm::ConstantStruct::get( llvm::StructType::getTypeByName( module->getContext(), layoutitem_struct), diff --git a/lib/codegen/Util.cpp b/lib/codegen/Util.cpp index d87cba163..93fe7640f 100644 --- a/lib/codegen/Util.cpp +++ b/lib/codegen/Util.cpp @@ -22,4 +22,18 @@ llvm::Function *kore_heap_alloc(std::string const &name, llvm::Module *module) { return get_or_insert_function(module, name, alloc_type); } +llvm::Constant *get_offset_of_member( + [[maybe_unused]] llvm::Module *mod, llvm::StructType *struct_ty, + int nth_member) { +#if LLVM_VERSION_MAJOR >= 17 + auto offset + = llvm::DataLayout(mod).getStructLayout(struct_ty)->getElementOffset( + nth_member); + auto *offset_ty = llvm::Type::getInt64Ty(mod->getContext()); + return llvm::ConstantInt::get(offset_ty, offset); +#else + return llvm::ConstantExpr::getOffsetOf(struct_ty, nth_member); +#endif +} + } // namespace kllvm diff --git a/runtime/collect/CMakeLists.txt b/runtime/collect/CMakeLists.txt index 06c3571c9..9f163872c 100644 --- a/runtime/collect/CMakeLists.txt +++ b/runtime/collect/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(collect STATIC collect.cpp - migrate_roots.cpp + migrate_static_roots.cpp migrate_collection.cpp ) diff --git a/runtime/collect/collect.cpp b/runtime/collect/collect.cpp index f7e6460b0..0ea7765e9 100644 --- a/runtime/collect/collect.cpp +++ b/runtime/collect/collect.cpp @@ -41,6 +41,14 @@ size_t get_size(uint64_t hdr, uint16_t layout) { return size_hdr(hdr); } +uint8_t get_first_field_offset(uint16_t layout_int) { + if (!layout_int) { + return 1; + } + layout *layout_data = get_layout_data(layout_int); + return layout_data->args[0].offset / 8; +} + void migrate(block **block_ptr) { block *curr_block = *block_ptr; if (is_leaf_block(curr_block) || !is_heap_block(curr_block)) { @@ -50,7 +58,8 @@ void migrate(block **block_ptr) { INITIALIZE_MIGRATE(); uint16_t layout = layout_hdr(hdr); size_t len_in_bytes = get_size(hdr, layout); - auto **forwarding_address = (block **)(curr_block + 1); + auto **forwarding_address + = (block **)(curr_block + get_first_field_offset(layout)); if (!hasForwardingAddress) { block *new_block = nullptr; if (shouldPromote || (isInOldGen && collect_old)) { @@ -199,14 +208,10 @@ static void migrate_floating(floating **floating_ptr) { *floating_ptr = *(floating **)(flt->f.f->_mpfr_d); } -static void migrate_child( - void *curr_block, layoutitem *args, unsigned i, bool ptr, bool is_block) { +static void +migrate_child(void *curr_block, layoutitem *args, unsigned i, bool ptr) { layoutitem *arg_data = args + i; void *arg = ((char *)curr_block) + arg_data->offset; - if (is_block) { - migrate((block **)arg); - return; - } switch (arg_data->cat) { case MAP_LAYOUT: migrate_map(ptr ? *(map **)arg : arg); break; case RANGEMAP_LAYOUT: migrate_rangemap(ptr ? *(rangemap **)arg : arg); break; @@ -223,6 +228,31 @@ static void migrate_child( } } +static void +migrate_root(void *curr_block, layoutitem *args, unsigned i, bool is_block) { + layoutitem *arg_data = args + i; + void *arg = ((char *)curr_block) + arg_data->offset; + if (is_block) { + migrate((block **)arg); + return; + } + switch (arg_data->cat) { + case MAP_LAYOUT: + case RANGEMAP_LAYOUT: + case LIST_LAYOUT: + case SET_LAYOUT: { + char *root_ptr = *(char **)arg; + auto *offset_ptr = (uint64_t *)(root_ptr - sizeof(uint64_t)); + uint64_t offset = *offset_ptr; + auto *base_ptr = (block *)(root_ptr - offset); + migrate((block **)&base_ptr); + *(void **)arg = (void *)((char *)base_ptr + offset); + break; + } + default: migrate_child(curr_block, args, i, true); break; + } +} + static char *evacuate(char *scan_ptr, char **alloc_ptr) { auto *curr_block = (block *)scan_ptr; uint64_t const hdr = curr_block->h.hdr; @@ -230,7 +260,7 @@ static char *evacuate(char *scan_ptr, char **alloc_ptr) { if (layout_int) { layout *layout_data = get_layout_data(layout_int); for (unsigned i = 0; i < layout_data->nargs; i++) { - migrate_child(curr_block, layout_data->args, i, false, false); + migrate_child(curr_block, layout_data->args, i, false); } } return move_ptr(scan_ptr, get_size(hdr, layout_int), *alloc_ptr); @@ -251,8 +281,6 @@ static bool should_collect_old_gen() { #endif } -void migrate_roots(); - void init_static_objects(void) { map m = map(); list l = list(); @@ -279,9 +307,9 @@ void kore_collect( #endif char *previous_oldspace_alloc_ptr = *old_alloc_ptr(); for (int i = 0; i < nroots; i++) { - migrate_child(roots, type_info, i, true, are_block[i]); + migrate_root(roots, type_info, i, are_block[i]); } - migrate_roots(); + migrate_static_roots(); char *scan_ptr = youngspace_ptr(); if (scan_ptr != *young_alloc_ptr()) { MEM_LOG("Evacuating young generation\n"); @@ -344,11 +372,13 @@ bool store_map_for_gc(void **roots, map *ptr) { *roots = ptr; return false; } - void *mem = kore_alloc(sizeof(blockheader) + sizeof(map)); + void *mem = kore_alloc(sizeof(blockheader) + sizeof(map) + sizeof(uint64_t)); auto *hdr = (blockheader *)mem; std::string name = get_raw_symbol_name(kllvm::sort_category::Map) + "{}"; *hdr = get_block_header_for_symbol(get_tag_for_symbol_name(name.c_str())); - auto *child = (map *)(hdr + 1); + auto *offset = (uint64_t *)(hdr + 1); + *offset = 16; + auto *child = (map *)(hdr + 2); *child = std::move(*ptr); *roots = mem; return true; @@ -359,11 +389,13 @@ bool store_set_for_gc(void **roots, set *ptr) { *roots = ptr; return false; } - void *mem = kore_alloc(sizeof(blockheader) + sizeof(set)); + void *mem = kore_alloc(sizeof(blockheader) + sizeof(set) + sizeof(uint64_t)); auto *hdr = (blockheader *)mem; std::string name = get_raw_symbol_name(kllvm::sort_category::Set) + "{}"; *hdr = get_block_header_for_symbol(get_tag_for_symbol_name(name.c_str())); - auto *child = (set *)(hdr + 1); + auto *offset = (uint64_t *)(hdr + 1); + *offset = 16; + auto *child = (set *)(hdr + 2); *child = std::move(*ptr); *roots = mem; return true; @@ -374,11 +406,13 @@ bool store_list_for_gc(void **roots, list *ptr) { *roots = ptr; return false; } - void *mem = kore_alloc(sizeof(blockheader) + sizeof(list)); + void *mem = kore_alloc(sizeof(blockheader) + sizeof(list) + sizeof(uint64_t)); auto *hdr = (blockheader *)mem; std::string name = get_raw_symbol_name(kllvm::sort_category::List) + "{}"; *hdr = get_block_header_for_symbol(get_tag_for_symbol_name(name.c_str())); - auto *child = (list *)(hdr + 1); + auto *offset = (uint64_t *)(hdr + 1); + *offset = 16; + auto *child = (list *)(hdr + 2); *child = std::move(*ptr); *roots = mem; return true; @@ -389,11 +423,14 @@ bool store_rangemap_for_gc(void **roots, rangemap *ptr) { *roots = ptr; return false; } - void *mem = kore_alloc(sizeof(blockheader) + sizeof(rangemap)); + void *mem + = kore_alloc(sizeof(blockheader) + sizeof(rangemap) + sizeof(uint64_t)); auto *hdr = (blockheader *)mem; std::string name = get_raw_symbol_name(kllvm::sort_category::RangeMap) + "{}"; *hdr = get_block_header_for_symbol(get_tag_for_symbol_name(name.c_str())); - auto *child = (rangemap *)(hdr + 1); + auto *offset = (uint64_t *)(hdr + 1); + *offset = 16; + auto *child = (rangemap *)(hdr + 2); *child = std::move(*ptr); *roots = mem; return true; @@ -402,7 +439,7 @@ bool store_rangemap_for_gc(void **roots, rangemap *ptr) { map *load_map_for_gc(void **roots, bool is_block) { void *mem = *roots; if (is_block) { - return (map *)(((char *)mem) + sizeof(blockheader)); + return (map *)(((char *)mem) + sizeof(blockheader) + sizeof(uint64_t)); } return (map *)mem; } @@ -410,7 +447,7 @@ map *load_map_for_gc(void **roots, bool is_block) { set *load_set_for_gc(void **roots, bool is_block) { void *mem = *roots; if (is_block) { - return (set *)(((char *)mem) + sizeof(blockheader)); + return (set *)(((char *)mem) + sizeof(blockheader) + sizeof(uint64_t)); } return (set *)mem; } @@ -418,7 +455,7 @@ set *load_set_for_gc(void **roots, bool is_block) { list *load_list_for_gc(void **roots, bool is_block) { void *mem = *roots; if (is_block) { - return (list *)(((char *)mem) + sizeof(blockheader)); + return (list *)(((char *)mem) + sizeof(blockheader) + sizeof(uint64_t)); } return (list *)mem; } @@ -426,7 +463,7 @@ list *load_list_for_gc(void **roots, bool is_block) { rangemap *load_rangemap_for_gc(void **roots, bool is_block) { void *mem = *roots; if (is_block) { - return (rangemap *)(((char *)mem) + sizeof(blockheader)); + return (rangemap *)(((char *)mem) + sizeof(blockheader) + sizeof(uint64_t)); } return (rangemap *)mem; } diff --git a/runtime/collect/migrate_roots.cpp b/runtime/collect/migrate_static_roots.cpp similarity index 94% rename from runtime/collect/migrate_roots.cpp rename to runtime/collect/migrate_static_roots.cpp index 853b82b09..d162f0bb8 100644 --- a/runtime/collect/migrate_roots.cpp +++ b/runtime/collect/migrate_static_roots.cpp @@ -9,9 +9,7 @@ extern bool kllvm_rand_state_initialized; extern "C" { -void migrate(block **block_ptr); - -void migrate_roots() { +void migrate_static_roots() { auto &l1 = list_impl::empty_root(); migrate_collection_node((void **)&l1); auto &l2 = list_impl::empty_tail(); diff --git a/test/defn/k-files/migrate-map-root.k b/test/defn/k-files/migrate-map-root.k new file mode 100644 index 000000000..08b3a0980 --- /dev/null +++ b/test/defn/k-files/migrate-map-root.k @@ -0,0 +1,14 @@ +module TEST + imports LIST + imports INT + imports BOOL + + configuration foo() baz(ListItem(3) ListItem(4)) 100000 + + syntax Pgm ::= foo() | bar(KItem, List) + syntax KItem ::= baz(List) + + rule foo() => bar(K, L) baz(L:List) #as K:KItem X => X -Int 1 + rule bar(_, _) => foo() X requires X >Int 0 + +endmodule diff --git a/test/defn/migrate-map-root.kore b/test/defn/migrate-map-root.kore new file mode 100644 index 000000000..e3a218fd0 --- /dev/null +++ b/test/defn/migrate-map-root.kore @@ -0,0 +1,2469 @@ +// RUN: %interpreter +// RUN: %check-diff +[topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + +module BASIC-K + sort SortK{} [] + sort SortKItem{} [] +endmodule +[] +module KSEQ + import BASIC-K [] + symbol kseq{}(SortKItem{}, SortK{}) : SortK{} [constructor{}(), functional{}(), injective{}()] + symbol dotk{}() : SortK{} [constructor{}(), functional{}(), injective{}()] + symbol append{}(SortK{}, SortK{}) : SortK{} [function{}(), functional{}()] + axiom {R} \implies{R}( + \and{R}( + \top{R}(), + \and{R}( + \in{SortK{}, R}(X0:SortK{}, dotk{}()), + \and{R}( + \in{SortK{}, R}(X1:SortK{}, TAIL:SortK{}), + \top{R}() + )) + ), + \equals{SortK{}, R}( + append{}(X0:SortK{}, X1:SortK{}), + \and{SortK{}}( + TAIL:SortK{}, + \top{SortK{}}() + ) + ) + ) [] + axiom {R} \implies{R}( + \and{R}( + \top{R}(), + \and{R}( + \in{SortK{}, R}(X0:SortK{}, kseq{}(K:SortKItem{}, KS:SortK{})), + \and{R}( + \in{SortK{}, R}(X1:SortK{}, TAIL:SortK{}), + \top{R}() + )) + ), + \equals{SortK{}, R}( + append{}(X0:SortK{}, X1:SortK{}), + \and{SortK{}}( + kseq{}(K:SortKItem{}, append{}(KS:SortK{}, TAIL:SortK{})), + \top{SortK{}}() + ) + ) + ) [] +endmodule +[] +module INJ + symbol inj{From, To}(From) : To [sortInjection{}()] + axiom {S1, S2, S3, R} \equals{S3, R}(inj{S2, S3}(inj{S1, S2}(T:S1)), inj{S1, S3}(T:S1)) [simplification{}()] +endmodule +[] +module K + import KSEQ [] + import INJ [] + alias weakExistsFinally{A}(A) : A where weakExistsFinally{A}(@X:A) := @X:A [] + alias weakAlwaysFinally{A}(A) : A where weakAlwaysFinally{A}(@X:A) := @X:A [] + alias allPathGlobally{A}(A) : A where allPathGlobally{A}(@X:A) := @X:A [] +endmodule +[] + +module TEST + +// imports + import K [] + +// sorts + sort SortKCellOpt{} [] + sort SortListCell{} [] + sort SortGeneratedTopCellFragment{} [] + hooked-sort SortList{} [concat{}(Lbl'Unds'List'Unds'{}()), element{}(LblListItem{}()), hook{}("LIST.List"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(913,3,913,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'List{}())] + sort SortListCellOpt{} [] + sort SortKCell{} [] + sort SortGeneratedTopCell{} [] + sort SortGeneratedCounterCell{} [] + sort SortCounterCell{} [] + hooked-sort SortMap{} [concat{}(Lbl'Unds'Map'Unds'{}()), element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), hook{}("MAP.Map"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(218,3,218,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Map{}())] + sort SortCounterCellOpt{} [] + sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/kast.md)"), token{}()] + hooked-sort SortInt{} [hasDomainValues{}(), hook{}("INT.Int"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1198,3,1198,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-sort SortSet{} [concat{}(Lbl'Unds'Set'Unds'{}()), element{}(LblSetItem{}()), hook{}("SET.Set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(700,3,700,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] + sort SortPgm{} [] + hooked-sort SortBool{} [hasDomainValues{}(), hook{}("BOOL.Bool"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1077,3,1077,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// symbols + hooked-symbol Lbl'Stop'List{}() : SortList{} [function{}(), functional{}(), hook{}("LIST.unit"), klabel{}(".List"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,121)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Stop'Map{}() : SortMap{} [function{}(), functional{}(), hook{}("MAP.unit"), klabel{}(".Map"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,104)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Stop'Set{}() : SortSet{} [function{}(), functional{}(), hook{}("SET.unit"), klabel{}(".Set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,98)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + symbol Lbl'-LT-'counter'-GT-'{}(SortInt{}) : SortCounterCell{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,75,6,102)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol Lbl'-LT-'generatedCounter'-GT-'{}(SortInt{}) : SortGeneratedCounterCell{} [constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortListCell{}, SortCounterCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,16,6,102)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol Lbl'-LT-'generatedTop'-GT-'-fragment{}(SortKCellOpt{}, SortListCellOpt{}, SortCounterCellOpt{}) : SortGeneratedTopCellFragment{} [constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,16,6,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol Lbl'-LT-'list'-GT-'{}(SortKItem{}) : SortListCell{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,31,6,74)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [function{}(), hook{}("LIST.get"), klabel{}("List:get"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,20,965,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("")] + hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [function{}(), hook{}("LIST.range"), klabel{}("List:range"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("")] + hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.element"), klabel{}("ListItem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_elem"), symbol'Kywd'{}(""), total{}()] + hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [function{}(), hook{}("MAP.lookup"), klabel{}("Map:lookup"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("")] + hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.update"), klabel{}("Map:update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,140)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.difference"), klabel{}("Set:difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [function{}(), functional{}(), hook{}("SET.in"), klabel{}("Set:in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,102)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.element"), injective{}(), klabel{}("SetItem"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tmod"), klabel{}("_%Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1246,18,1246,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("")] + hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.and"), klabel{}("_&Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1257,18,1257,133)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("andInt"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.mul"), klabel{}("_*Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,130)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("*"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.add"), klabel{}("_+Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1251,18,1251,130)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("+"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.sub"), klabel{}("_-Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("-"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(311,18,311,88)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tdiv"), klabel{}("_/Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1245,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("")] + hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shl"), klabel{}("_<=Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1315,19,1315,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}(">="), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shr"), klabel{}("_>>Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1254,18,1254,121)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shrInt"), symbol'Kywd'{}("")] + hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), functional{}(), hook{}("INT.gt"), klabel{}("_>Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1316,19,1316,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}(">"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [element{}(LblListItem{}()), function{}(), functional{}(), hook{}("LIST.concat"), klabel{}("_List_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,188)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_concat"), symbol'Kywd'{}(""), total{}(), unit{}(Lbl'Stop'List{}())] + hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), function{}(), hook{}("MAP.concat"), klabel{}("_Map_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,173)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), unit{}(Lbl'Stop'Map{}())] + hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [element{}(LblSetItem{}()), function{}(), hook{}("SET.concat"), idem{}(), klabel{}("_Set_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), unit{}(Lbl'Stop'Set{}())] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.update"), klabel{}("List:set"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.remove"), klabel{}("_[_<-undef]"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), klabel{}("Map:lookupOrDefault"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.powmod"), klabel{}("_^%Int__"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,139)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}("")] + hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.pow"), klabel{}("_^Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("^"), symbol'Kywd'{}("")] + hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.and"), klabel{}("_andBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1110,19,1110,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.andThen"), klabel{}("_andThenBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1111,19,1111,154)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.ediv"), klabel{}("_divInt_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1248,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("")] + symbol Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1327,19,1327,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.implies"), klabel{}("_impliesBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1115,19,1115,153)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("=>"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(SortKItem{}, SortList{}) : SortBool{} [function{}(), functional{}(), hook{}("LIST.in"), klabel{}("_inList_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1021,19,1021,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(SortKItem{}, SortMap{}) : SortBool{} [function{}(), functional{}(), hook{}("MAP.in_keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(357,19,357,89)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.emod"), klabel{}("_modInt_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1249,18,1249,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("")] + hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.or"), klabel{}("_orBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1113,19,1113,143)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.orElse"), klabel{}("_orElseBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1114,19,1114,151)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.xor"), klabel{}("_xorBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1112,19,1112,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("xor"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.xor"), klabel{}("_xorInt_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1259,18,1259,135)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("xorInt"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.element"), injective{}(), klabel{}("_|->_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,127)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsPipe'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.or"), klabel{}("_|Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("orInt"), symbol'Kywd'{}(""), total{}()] + hooked-symbol Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.union"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(748,18,748,92)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.abs"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1278,18,1278,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), total{}()] + symbol Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(SortKItem{}, SortList{}) : SortPgm{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,25,8,41)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(SortList{}) : SortKItem{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,19,9,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + hooked-symbol LblbitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.bitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1303,18,1303,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lblchoice'LParUndsRParUnds'MAP'Unds'KItem'Unds'Map{}(SortMap{}) : SortKItem{} [function{}(), hook{}("MAP.choice"), klabel{}("Map:choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lblchoice'LParUndsRParUnds'SET'Unds'KItem'Unds'Set{}(SortSet{}) : SortKItem{} [function{}(), hook{}("SET.choice"), klabel{}("Set:choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblfillList'LParUndsCommUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'Int'Unds'KItem{}(SortList{}, SortInt{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.fill"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1002,19,1002,100)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol Lblfoo'LParRParUnds'TEST'Unds'Pgm{}() : SortPgm{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,17,8,22)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [freshGenerator{}(), function{}(), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1441,18,1441,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol LblgetGeneratedCounterCell{}(SortGeneratedTopCell{}) : SortGeneratedCounterCell{} [function{}()] + symbol LblinitCounterCell{}() : SortCounterCell{} [function{}()] + symbol LblinitGeneratedCounterCell{}() : SortGeneratedCounterCell{} [function{}()] + symbol LblinitGeneratedTopCell{}() : SortGeneratedTopCell{} [function{}()] + symbol LblinitKCell{}() : SortKCell{} [function{}()] + symbol LblinitListCell{}() : SortListCell{} [function{}()] + hooked-symbol LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.intersection"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(759,18,759,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol LblisBool{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisCounterCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisCounterCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisGeneratedCounterCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisGeneratedTopCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisGeneratedTopCellFragment{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisInt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisK{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisKCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisKCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisKConfigVar{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisKItem{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisList{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisListCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisListCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisMap{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisPgm{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisSet{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + hooked-symbol Lblite{SortSort}(SortBool{}, SortSort, SortSort) : SortSort [function{}(), functional{}(), hook{}("KEQUAL.ite"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2291,26,2291,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("ite"), symbol'Kywd'{}("ite"), total{}()] + hooked-symbol Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(SortMap{}) : SortSet{} [function{}(), functional{}(), hook{}("MAP.keys"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(341,18,341,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.keys_list"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(349,19,349,80)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbllog2Int'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.log2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1289,18,1289,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblmakeList'LParUndsCommUndsRParUnds'LIST'Unds'List'Unds'Int'Unds'KItem{}(SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.make"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(983,19,983,82)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.max"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1270,18,1270,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #2 #1)"), total{}()] + hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.min"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1269,18,1269,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #1 #2)"), total{}()] + symbol LblnoCounterCell{}() : SortCounterCellOpt{} [constructor{}(), functional{}(), injective{}()] + symbol LblnoKCell{}() : SortKCellOpt{} [constructor{}(), functional{}(), injective{}()] + symbol LblnoListCell{}() : SortListCellOpt{} [constructor{}(), functional{}(), injective{}()] + hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.not"), klabel{}("notBool_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1109,19,1109,139)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("not"), symbol'Kywd'{}(""), total{}()] + symbol Lblproject'Coln'Bool{}(SortK{}) : SortBool{} [function{}()] + symbol Lblproject'Coln'CounterCell{}(SortK{}) : SortCounterCell{} [function{}()] + symbol Lblproject'Coln'CounterCellOpt{}(SortK{}) : SortCounterCellOpt{} [function{}()] + symbol Lblproject'Coln'GeneratedCounterCell{}(SortK{}) : SortGeneratedCounterCell{} [function{}()] + symbol Lblproject'Coln'GeneratedTopCell{}(SortK{}) : SortGeneratedTopCell{} [function{}()] + symbol Lblproject'Coln'GeneratedTopCellFragment{}(SortK{}) : SortGeneratedTopCellFragment{} [function{}()] + symbol Lblproject'Coln'Int{}(SortK{}) : SortInt{} [function{}()] + symbol Lblproject'Coln'K{}(SortK{}) : SortK{} [function{}()] + symbol Lblproject'Coln'KCell{}(SortK{}) : SortKCell{} [function{}()] + symbol Lblproject'Coln'KCellOpt{}(SortK{}) : SortKCellOpt{} [function{}()] + symbol Lblproject'Coln'KItem{}(SortK{}) : SortKItem{} [function{}()] + symbol Lblproject'Coln'List{}(SortK{}) : SortList{} [function{}()] + symbol Lblproject'Coln'ListCell{}(SortK{}) : SortListCell{} [function{}()] + symbol Lblproject'Coln'ListCellOpt{}(SortK{}) : SortListCellOpt{} [function{}()] + symbol Lblproject'Coln'Map{}(SortK{}) : SortMap{} [function{}()] + symbol Lblproject'Coln'Pgm{}(SortK{}) : SortPgm{} [function{}()] + symbol Lblproject'Coln'Set{}(SortK{}) : SortSet{} [function{}()] + hooked-symbol LblpushList{}(SortKItem{}, SortList{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.push"), klabel{}("pushList"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(953,19,953,107)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(""), total{}()] + hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.rand"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1337,18,1337,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(SortMap{}, SortSet{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.removeAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(333,18,333,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblsignExtendBitRangeInt'LParUndsCommUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.signExtendBitRange"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1304,18,1304,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(SortList{}) : SortInt{} [function{}(), functional{}(), hook{}("LIST.size"), klabel{}("sizeList"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1029,18,1029,117)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_len"), total{}()] + hooked-symbol Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(SortMap{}) : SortInt{} [function{}(), functional{}(), hook{}("MAP.size"), klabel{}("sizeMap"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(SortSet{}) : SortInt{} [function{}(), functional{}(), hook{}("SET.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(794,18,794,76)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [function{}(), hook{}("INT.srand"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1338,16,1338,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblupdateList'LParUndsCommUndsCommUndsRParUnds'LIST'Unds'List'Unds'List'Unds'Int'Unds'List{}(SortList{}, SortInt{}, SortList{}) : SortList{} [function{}(), hook{}("LIST.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(993,19,993,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(SortMap{}, SortMap{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.updateAll"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(324,18,324,87)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lblvalues'LParUndsRParUnds'MAP'Unds'List'Unds'Map{}(SortMap{}) : SortList{} [function{}(), hook{}("MAP.values"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(365,19,365,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.not"), klabel{}("~Int_"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,120)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("notInt"), symbol'Kywd'{}(""), total{}()] + +// generated axioms + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCellOpt{}, SortKItem{}} (From:SortKCellOpt{}))) [subsort{SortKCellOpt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortCounterCellOpt{}, \equals{SortCounterCellOpt{}, R} (Val:SortCounterCellOpt{}, inj{SortCounterCell{}, SortCounterCellOpt{}} (From:SortCounterCell{}))) [subsort{SortCounterCell{}, SortCounterCellOpt{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKCell{}, SortKItem{}} (From:SortKCell{}))) [subsort{SortKCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortListCellOpt{}, SortKItem{}} (From:SortListCellOpt{}))) [subsort{SortListCellOpt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKCellOpt{}, \equals{SortKCellOpt{}, R} (Val:SortKCellOpt{}, inj{SortKCell{}, SortKCellOpt{}} (From:SortKCell{}))) [subsort{SortKCell{}, SortKCellOpt{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortSet{}, SortKItem{}} (From:SortSet{}))) [subsort{SortSet{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (From:SortGeneratedCounterCell{}))) [subsort{SortGeneratedCounterCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortCounterCellOpt{}, SortKItem{}} (From:SortCounterCellOpt{}))) [subsort{SortCounterCellOpt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedTopCell{}, SortKItem{}} (From:SortGeneratedTopCell{}))) [subsort{SortGeneratedTopCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortCounterCell{}, SortKItem{}} (From:SortCounterCell{}))) [subsort{SortCounterCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortList{}, SortKItem{}} (From:SortList{}))) [subsort{SortList{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortBool{}, SortKItem{}} (From:SortBool{}))) [subsort{SortBool{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortListCellOpt{}, \equals{SortListCellOpt{}, R} (Val:SortListCellOpt{}, inj{SortListCell{}, SortListCellOpt{}} (From:SortListCell{}))) [subsort{SortListCell{}, SortListCellOpt{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortInt{}, SortKItem{}} (From:SortInt{}))) [subsort{SortInt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (From:SortGeneratedTopCellFragment{}))) [subsort{SortGeneratedTopCellFragment{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortPgm{}, SortKItem{}} (From:SortPgm{}))) [subsort{SortPgm{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortMap{}, SortKItem{}} (From:SortMap{}))) [subsort{SortMap{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortListCell{}, SortKItem{}} (From:SortListCell{}))) [subsort{SortListCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortKConfigVar{}, SortKItem{}} (From:SortKConfigVar{}))) [subsort{SortKConfigVar{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, Lbl'Stop'List{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'Stop'Map{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lbl'Stop'Set{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortCounterCell{}, \equals{SortCounterCell{}, R} (Val:SortCounterCell{}, Lbl'-LT-'counter'-GT-'{}(K0:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortCounterCell{}} (\and{SortCounterCell{}} (Lbl'-LT-'counter'-GT-'{}(X0:SortInt{}), Lbl'-LT-'counter'-GT-'{}(Y0:SortInt{})), Lbl'-LT-'counter'-GT-'{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortGeneratedCounterCell{}, \equals{SortGeneratedCounterCell{}, R} (Val:SortGeneratedCounterCell{}, Lbl'-LT-'generatedCounter'-GT-'{}(K0:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortGeneratedCounterCell{}} (\and{SortGeneratedCounterCell{}} (Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{}), Lbl'-LT-'generatedCounter'-GT-'{}(Y0:SortInt{})), Lbl'-LT-'generatedCounter'-GT-'{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortGeneratedTopCell{}, \equals{SortGeneratedTopCell{}, R} (Val:SortGeneratedTopCell{}, Lbl'-LT-'generatedTop'-GT-'{}(K0:SortKCell{}, K1:SortListCell{}, K2:SortCounterCell{}, K3:SortGeneratedCounterCell{}))) [functional{}()] // functional + axiom{}\implies{SortGeneratedTopCell{}} (\and{SortGeneratedTopCell{}} (Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortListCell{}, X2:SortCounterCell{}, X3:SortGeneratedCounterCell{}), Lbl'-LT-'generatedTop'-GT-'{}(Y0:SortKCell{}, Y1:SortListCell{}, Y2:SortCounterCell{}, Y3:SortGeneratedCounterCell{})), Lbl'-LT-'generatedTop'-GT-'{}(\and{SortKCell{}} (X0:SortKCell{}, Y0:SortKCell{}), \and{SortListCell{}} (X1:SortListCell{}, Y1:SortListCell{}), \and{SortCounterCell{}} (X2:SortCounterCell{}, Y2:SortCounterCell{}), \and{SortGeneratedCounterCell{}} (X3:SortGeneratedCounterCell{}, Y3:SortGeneratedCounterCell{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortGeneratedTopCellFragment{}, \equals{SortGeneratedTopCellFragment{}, R} (Val:SortGeneratedTopCellFragment{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(K0:SortKCellOpt{}, K1:SortListCellOpt{}, K2:SortCounterCellOpt{}))) [functional{}()] // functional + axiom{}\implies{SortGeneratedTopCellFragment{}} (\and{SortGeneratedTopCellFragment{}} (Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortListCellOpt{}, X2:SortCounterCellOpt{}), Lbl'-LT-'generatedTop'-GT-'-fragment{}(Y0:SortKCellOpt{}, Y1:SortListCellOpt{}, Y2:SortCounterCellOpt{})), Lbl'-LT-'generatedTop'-GT-'-fragment{}(\and{SortKCellOpt{}} (X0:SortKCellOpt{}, Y0:SortKCellOpt{}), \and{SortListCellOpt{}} (X1:SortListCellOpt{}, Y1:SortListCellOpt{}), \and{SortCounterCellOpt{}} (X2:SortCounterCellOpt{}, Y2:SortCounterCellOpt{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortKCell{}, \equals{SortKCell{}, R} (Val:SortKCell{}, Lbl'-LT-'k'-GT-'{}(K0:SortK{}))) [functional{}()] // functional + axiom{}\implies{SortKCell{}} (\and{SortKCell{}} (Lbl'-LT-'k'-GT-'{}(X0:SortK{}), Lbl'-LT-'k'-GT-'{}(Y0:SortK{})), Lbl'-LT-'k'-GT-'{}(\and{SortK{}} (X0:SortK{}, Y0:SortK{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortListCell{}, \equals{SortListCell{}, R} (Val:SortListCell{}, Lbl'-LT-'list'-GT-'{}(K0:SortKItem{}))) [functional{}()] // functional + axiom{}\implies{SortListCell{}} (\and{SortListCell{}} (Lbl'-LT-'list'-GT-'{}(X0:SortKItem{}), Lbl'-LT-'list'-GT-'{}(Y0:SortKItem{})), Lbl'-LT-'list'-GT-'{}(\and{SortKItem{}} (X0:SortKItem{}, Y0:SortKItem{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, LblListItem{}(K0:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblMap'Coln'update{}(K0:SortMap{}, K1:SortKItem{}, K2:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblSet'Coln'difference{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblSet'Coln'in{}(K0:SortKItem{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblSetItem{}(K0:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'UndsAnd-'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'UndsStar'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'UndsPlus'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Unds'-Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'Unds'-Map'UndsUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-Eqls'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-Eqls'Map'UndsUnds'MAP'Unds'Bool'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-Eqls'Set'UndsUnds'SET'Unds'Bool'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-LT-'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsSlshEqls'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsSlshEqls'K'Unds'{}(K0:SortK{}, K1:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsEqls'Bool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsEqls'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'UndsEqlsEqls'K'Unds'{}(K0:SortK{}, K1:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-GT-Eqls'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds-GT-'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(Lbl'Unds'List'Unds'{}(K1:SortList{},K2:SortList{}),K3:SortList{}),Lbl'Unds'List'Unds'{}(K1:SortList{},Lbl'Unds'List'Unds'{}(K2:SortList{},K3:SortList{}))) [assoc{}()] // associativity + axiom{R}\equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(K:SortList{},Lbl'Stop'List{}()),K:SortList{}) [unit{}()] // right unit + axiom{R}\equals{SortList{}, R} (Lbl'Unds'List'Unds'{}(Lbl'Stop'List{}(),K:SortList{}),K:SortList{}) [unit{}()] // left unit + axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, Lbl'Unds'List'Unds'{}(K0:SortList{}, K1:SortList{}))) [functional{}()] // functional + axiom{R} \equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(K1:SortMap{},K2:SortMap{}),K3:SortMap{}),Lbl'Unds'Map'Unds'{}(K1:SortMap{},Lbl'Unds'Map'Unds'{}(K2:SortMap{},K3:SortMap{}))) [assoc{}()] // associativity + axiom{R}\equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(K:SortMap{},Lbl'Stop'Map{}()),K:SortMap{}) [unit{}()] // right unit + axiom{R}\equals{SortMap{}, R} (Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),K:SortMap{}),K:SortMap{}) [unit{}()] // left unit + axiom{R} \equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(Lbl'Unds'Set'Unds'{}(K1:SortSet{},K2:SortSet{}),K3:SortSet{}),Lbl'Unds'Set'Unds'{}(K1:SortSet{},Lbl'Unds'Set'Unds'{}(K2:SortSet{},K3:SortSet{}))) [assoc{}()] // associativity + axiom{R} \equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(K:SortSet{},K:SortSet{}),K:SortSet{}) [idem{}()] // idempotency + axiom{R}\equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(K:SortSet{},Lbl'Stop'Set{}()),K:SortSet{}) [unit{}()] // right unit + axiom{R}\equals{SortSet{}, R} (Lbl'Unds'Set'Unds'{}(Lbl'Stop'Set{}(),K:SortSet{}),K:SortSet{}) [unit{}()] // left unit + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(K0:SortMap{}, K1:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lbl'UndsLSqBUndsRSqB'orDefault'UndsUnds'MAP'Unds'KItem'Unds'Map'Unds'KItem'Unds'KItem{}(K0:SortMap{}, K1:SortKItem{}, K2:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'andBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'andThenBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'impliesBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'in'UndsUnds'LIST'Unds'Bool'Unds'KItem'Unds'List{}(K0:SortKItem{}, K1:SortList{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'Unds'Bool'Unds'KItem'Unds'Map{}(K0:SortKItem{}, K1:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'orBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'orElseBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, Lbl'Unds'xorBool'Unds'{}(K0:SortBool{}, K1:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Unds'xorInt'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, Lbl'UndsPipe'-'-GT-Unds'{}(K0:SortKItem{}, K1:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'UndsPipe'Int'Unds'{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(K0:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortPgm{}, \equals{SortPgm{}, R} (Val:SortPgm{}, Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(K0:SortKItem{}, K1:SortList{}))) [functional{}()] // functional + axiom{}\implies{SortPgm{}} (\and{SortPgm{}} (Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(X0:SortKItem{}, X1:SortList{}), Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(Y0:SortKItem{}, Y1:SortList{})), Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(\and{SortKItem{}} (X0:SortKItem{}, Y0:SortKItem{}), \and{SortList{}} (X1:SortList{}, Y1:SortList{}))) [constructor{}()] // no confusion same constructor + axiom{}\not{SortPgm{}} (\and{SortPgm{}} (Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(X0:SortKItem{}, X1:SortList{}), Lblfoo'LParRParUnds'TEST'Unds'Pgm{}())) [constructor{}()] // no confusion different constructors + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(K0:SortList{}))) [functional{}()] // functional + axiom{}\implies{SortKItem{}} (\and{SortKItem{}} (Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(X0:SortList{}), Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(Y0:SortList{})), Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(\and{SortList{}} (X0:SortList{}, Y0:SortList{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortPgm{}, \equals{SortPgm{}, R} (Val:SortPgm{}, Lblfoo'LParRParUnds'TEST'Unds'Pgm{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(K0:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, LblintersectSet'LParUndsCommUndsRParUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(K0:SortSet{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisBool{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisCounterCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisCounterCellOpt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedCounterCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedTopCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisGeneratedTopCellFragment{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisInt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisK{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKCellOpt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKConfigVar{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisKItem{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisList{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisListCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisListCellOpt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisMap{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisPgm{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisSet{}(K0:SortK{}))) [functional{}()] // functional + axiom{R, SortSort} \exists{R} (Val:SortSort, \equals{SortSort, R} (Val:SortSort, Lblite{SortSort}(K0:SortBool{}, K1:SortSort, K2:SortSort))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortSet{}, \equals{SortSet{}, R} (Val:SortSet{}, Lblkeys'LParUndsRParUnds'MAP'Unds'Set'Unds'Map{}(K0:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortCounterCellOpt{}, \equals{SortCounterCellOpt{}, R} (Val:SortCounterCellOpt{}, LblnoCounterCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortKCellOpt{}, \equals{SortKCellOpt{}, R} (Val:SortKCellOpt{}, LblnoKCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortListCellOpt{}, \equals{SortListCellOpt{}, R} (Val:SortListCellOpt{}, LblnoListCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblnotBool'Unds'{}(K0:SortBool{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, LblpushList{}(K0:SortKItem{}, K1:SortList{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblremoveAll'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Set{}(K0:SortMap{}, K1:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'LIST'Unds'Int'Unds'List{}(K0:SortList{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'MAP'Unds'Int'Unds'Map{}(K0:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lblsize'LParUndsRParUnds'SET'Unds'Int'Unds'Set{}(K0:SortSet{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortMap{}, \equals{SortMap{}, R} (Val:SortMap{}, LblupdateMap'LParUndsCommUndsRParUnds'MAP'Unds'Map'Unds'Map'Unds'Map{}(K0:SortMap{}, K1:SortMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, Lbl'Tild'Int'Unds'{}(K0:SortInt{}))) [functional{}()] // functional + axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortCounterCell{}} (\exists{SortCounterCell{}} (X0:SortInt{}, Lbl'-LT-'counter'-GT-'{}(X0:SortInt{})), \bottom{SortCounterCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortCounterCellOpt{}} (LblnoCounterCell{}(), \exists{SortCounterCellOpt{}} (Val:SortCounterCell{}, inj{SortCounterCell{}, SortCounterCellOpt{}} (Val:SortCounterCell{})), \bottom{SortCounterCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedCounterCell{}} (\exists{SortGeneratedCounterCell{}} (X0:SortInt{}, Lbl'-LT-'generatedCounter'-GT-'{}(X0:SortInt{})), \bottom{SortGeneratedCounterCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedTopCell{}} (\exists{SortGeneratedTopCell{}} (X0:SortKCell{}, \exists{SortGeneratedTopCell{}} (X1:SortListCell{}, \exists{SortGeneratedTopCell{}} (X2:SortCounterCell{}, \exists{SortGeneratedTopCell{}} (X3:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortListCell{}, X2:SortCounterCell{}, X3:SortGeneratedCounterCell{}))))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortListCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X2:SortCounterCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortListCellOpt{}, X2:SortCounterCellOpt{})))), \bottom{SortGeneratedTopCellFragment{}}()) [constructor{}()] // no junk + axiom{} \or{SortInt{}} (\top{SortInt{}}(), \bottom{SortInt{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortKCell{}} (\exists{SortKCell{}} (X0:SortK{}, Lbl'-LT-'k'-GT-'{}(X0:SortK{})), \bottom{SortKCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortKCellOpt{}} (LblnoKCell{}(), \exists{SortKCellOpt{}} (Val:SortKCell{}, inj{SortKCell{}, SortKCellOpt{}} (Val:SortKCell{})), \bottom{SortKCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortKConfigVar{}} (\top{SortKConfigVar{}}(), \bottom{SortKConfigVar{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + axiom{} \or{SortKItem{}} (\exists{SortKItem{}} (X0:SortList{}, Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(X0:SortList{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \exists{SortKItem{}} (Val:SortCounterCell{}, inj{SortCounterCell{}, SortKItem{}} (Val:SortCounterCell{})), \exists{SortKItem{}} (Val:SortCounterCellOpt{}, inj{SortCounterCellOpt{}, SortKItem{}} (Val:SortCounterCellOpt{})), \exists{SortKItem{}} (Val:SortGeneratedCounterCell{}, inj{SortGeneratedCounterCell{}, SortKItem{}} (Val:SortGeneratedCounterCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCell{}, inj{SortGeneratedTopCell{}, SortKItem{}} (Val:SortGeneratedTopCell{})), \exists{SortKItem{}} (Val:SortGeneratedTopCellFragment{}, inj{SortGeneratedTopCellFragment{}, SortKItem{}} (Val:SortGeneratedTopCellFragment{})), \exists{SortKItem{}} (Val:SortInt{}, inj{SortInt{}, SortKItem{}} (Val:SortInt{})), \exists{SortKItem{}} (Val:SortKCell{}, inj{SortKCell{}, SortKItem{}} (Val:SortKCell{})), \exists{SortKItem{}} (Val:SortKCellOpt{}, inj{SortKCellOpt{}, SortKItem{}} (Val:SortKCellOpt{})), \exists{SortKItem{}} (Val:SortKConfigVar{}, inj{SortKConfigVar{}, SortKItem{}} (Val:SortKConfigVar{})), \exists{SortKItem{}} (Val:SortList{}, inj{SortList{}, SortKItem{}} (Val:SortList{})), \exists{SortKItem{}} (Val:SortListCell{}, inj{SortListCell{}, SortKItem{}} (Val:SortListCell{})), \exists{SortKItem{}} (Val:SortListCellOpt{}, inj{SortListCellOpt{}, SortKItem{}} (Val:SortListCellOpt{})), \exists{SortKItem{}} (Val:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortPgm{}, inj{SortPgm{}, SortKItem{}} (Val:SortPgm{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortListCell{}} (\exists{SortListCell{}} (X0:SortKItem{}, Lbl'-LT-'list'-GT-'{}(X0:SortKItem{})), \bottom{SortListCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortListCellOpt{}} (LblnoListCell{}(), \exists{SortListCellOpt{}} (Val:SortListCell{}, inj{SortListCell{}, SortListCellOpt{}} (Val:SortListCell{})), \bottom{SortListCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortPgm{}} (\exists{SortPgm{}} (X0:SortKItem{}, \exists{SortPgm{}} (X1:SortList{}, Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(X0:SortKItem{}, X1:SortList{}))), Lblfoo'LParRParUnds'TEST'Unds'Pgm{}(), \bottom{SortPgm{}}()) [constructor{}()] // no junk + +// rules +// rule ``(``(inj{Pgm,KItem}(`bar(_,_)_TEST_Pgm_KItem_List`(_Gen0,_Gen1))),_Gen2,``(X) #as _Gen8,_Gen3)=>``(``(inj{Pgm,KItem}(`foo()_TEST_Pgm`(.KList))),_Gen2,_Gen8,_Gen3) requires `_>Int_`(X,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(7d3b05f1e147d2d3749cc861930293c7c6f6c6f879fb7ac09638955d12baf955), org.kframework.attributes.Location(Location(12,7,12,75)), org.kframework.attributes.Source(Source(/home/dwightguth/test/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(Var'Unds'Gen0:SortKItem{},Var'Unds'Gen1:SortList{})),dotk{}())),Var'Unds'Gen2:SortListCell{},\and{SortCounterCell{}}(Lbl'-LT-'counter'-GT-'{}(VarX:SortInt{}),Var'Unds'Gen8:SortCounterCell{}),Var'Unds'Gen3:SortGeneratedCounterCell{}), + \equals{SortBool{},SortGeneratedTopCell{}}( + Lbl'Unds-GT-'Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("0")), + \dv{SortBool{}}("true"))), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblfoo'LParRParUnds'TEST'Unds'Pgm{}()),dotk{}())),Var'Unds'Gen2:SortListCell{},Var'Unds'Gen8:SortCounterCell{},Var'Unds'Gen3:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("7d3b05f1e147d2d3749cc861930293c7c6f6c6f879fb7ac09638955d12baf955"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(12,7,12,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + +// rule ``(``(inj{Pgm,KItem}(`foo()_TEST_Pgm`(.KList))),``(`baz(_)_TEST_KItem_List`(L) #as K),``(X),_DotVar0)=>``(``(inj{Pgm,KItem}(`bar(_,_)_TEST_Pgm_KItem_List`(K,L))),``(K),``(`_-Int_`(X,#token("1","Int"))),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fa2051eaa353be0022b102e570eabd4aaf6abe7fcee3e2feacd4795c13bb815c), org.kframework.attributes.Location(Location(11,7,11,108)), org.kframework.attributes.Source(Source(/home/dwightguth/test/test.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblfoo'LParRParUnds'TEST'Unds'Pgm{}()),dotk{}())),Lbl'-LT-'list'-GT-'{}(\and{SortKItem{}}(Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(VarL:SortList{}),VarK:SortKItem{})),Lbl'-LT-'counter'-GT-'{}(VarX:SortInt{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \top{SortGeneratedTopCell{}}()), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblbar'LParUndsCommUndsRParUnds'TEST'Unds'Pgm'Unds'KItem'Unds'List{}(VarK:SortKItem{},VarL:SortList{})),dotk{}())),Lbl'-LT-'list'-GT-'{}(VarK:SortKItem{}),Lbl'-LT-'counter'-GT-'{}(Lbl'Unds'-Int'Unds'{}(VarX:SortInt{},\dv{SortInt{}}("1"))),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("fa2051eaa353be0022b102e570eabd4aaf6abe7fcee3e2feacd4795c13bb815c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(11,7,11,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/test/test.k)")] + +// rule `_=/=Bool_`(B1,B2)=>`notBool_`(`_==Bool_`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f), org.kframework.attributes.Location(Location(1159,8,1159,57)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + VarB1:SortBool{} + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB2:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'UndsEqlsSlshEqls'Bool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Bool'Unds'{}(VarB1:SortBool{},VarB2:SortBool{})), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("31fe72efcfddcd8588a11d9d10c1b1a9f96ae3da46b647d4cb9d1e8b1bd1654f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1159,8,1159,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_=/=Int_`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3), org.kframework.attributes.Location(Location(1438,8,1438,53)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI1:SortInt{} + ),\and{R} ( + \in{SortInt{}, R} ( + X1:SortInt{}, + VarI2:SortInt{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'UndsEqlsSlshEqls'Int'Unds'{}(X0:SortInt{},X1:SortInt{}), + \and{SortBool{}} ( + LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarI1:SortInt{},VarI2:SortInt{})), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("4de6e05b11cdbed7ef5cb4c952127924661af4744c1e495370e1c8a962ba7be3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1438,8,1438,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_=/=K_`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c), org.kframework.attributes.Location(Location(2316,8,2316,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK1:SortK{} + ),\and{R} ( + \in{SortK{}, R} ( + X1:SortK{}, + VarK2:SortK{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'UndsEqlsSlshEqls'K'Unds'{}(X0:SortK{},X1:SortK{}), + \and{SortBool{}} ( + LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'K'Unds'{}(VarK1:SortK{},VarK2:SortK{})), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("bccaba7335e4cd77501a0667f2f7b3eb4a2105d5f60d804915dd4b1b08902c0c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2316,8,2316,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_andBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497), org.kframework.attributes.Location(Location(1132,8,1132,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \and{SortBool{}}(\dv{SortBool{}}("false"),Var'Unds'Gen1:SortBool{}) + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + Var'Unds'Gen0:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'andBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + Var'Unds'Gen1:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("61fbef33b3611f1cc2aaf3b5e8ddec4a0f434c557278c38461c65c8722743497"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1132,8,1132,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281), org.kframework.attributes.Location(Location(1131,8,1131,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'andBool'Unds'{}(VarB:SortBool{},\dv{SortBool{}}("true")), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("72139ee1f2b9362a47514de6503329ccf3c27e74e3ebfa0c0fe26321ec13f281"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1131,8,1131,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_andBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12), org.kframework.attributes.Location(Location(1133,8,1133,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'andBool'Unds'{}(Var'Unds'Gen0:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("fd61c826168aab115cd7f528702e8187ca16195bdcf29f42f33a32c83afebb12"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1133,8,1133,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f), org.kframework.attributes.Location(Location(1130,8,1130,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'andBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("5b9db8dba12010819161cc42dadccd0adf0100a47c21f884ae66c0a3d5483a1f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1130,8,1130,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_andThenBool_`(#token("false","Bool") #as _Gen1,_Gen0)=>_Gen1 requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d), org.kframework.attributes.Location(Location(1137,8,1137,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \and{SortBool{}}(\dv{SortBool{}}("false"),Var'Unds'Gen1:SortBool{}) + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + Var'Unds'Gen0:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'andThenBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + Var'Unds'Gen1:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("5b729746be7bf2183d9eff138d97078a7c9489def6d8b2e1495c41ce3954997d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1137,8,1137,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_andThenBool_`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f), org.kframework.attributes.Location(Location(1136,8,1136,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'andThenBool'Unds'{}(VarK:SortBool{},\dv{SortBool{}}("true")), + \and{SortBool{}} ( + VarK:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2cfb33affb9c668d39a4a7267156085e1dbd3584fc7925b1aa9a1672bb9eab9f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1136,8,1136,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_andThenBool_`(_Gen0,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01), org.kframework.attributes.Location(Location(1138,8,1138,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'andThenBool'Unds'{}(Var'Unds'Gen0:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("198861009d03d8f5220000f16342962720be289ca0d49b12953fb2693e2fea01"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1138,8,1138,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_andThenBool_`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689), org.kframework.attributes.Location(Location(1135,8,1135,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarK:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'andThenBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarK:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("78a3191cbbdec57b0f411f41291076c8124bb0d9b6b57905674b2c6858d78689"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1135,8,1135,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_divInt_`(I1,I2)=>`_/Int_`(`_-Int_`(I1,`_modInt_`(I1,I2)),I2) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4), org.kframework.attributes.Location(Location(1427,8,1428,23)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \equals{SortBool{},R}( + Lbl'UndsEqlsSlshEqls'Int'Unds'{}(VarI2:SortInt{},\dv{SortInt{}}("0")), + \dv{SortBool{}}("true")), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI1:SortInt{} + ),\and{R} ( + \in{SortInt{}, R} ( + X1:SortInt{}, + VarI2:SortInt{} + ), + \top{R} () + ))), + \equals{SortInt{},R} ( + Lbl'Unds'divInt'Unds'{}(X0:SortInt{},X1:SortInt{}), + \and{SortInt{}} ( + Lbl'UndsSlsh'Int'Unds'{}(Lbl'Unds'-Int'Unds'{}(VarI1:SortInt{},Lbl'Unds'modInt'Unds'{}(VarI1:SortInt{},VarI2:SortInt{})),VarI2:SortInt{}), + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("83dcf9bc8c69f131715bc7a92d06c99b9a2b5f4c4fdafb69e6fdb2f1822712d4"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1427,8,1428,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_dividesInt__INT-COMMON_Bool_Int_Int`(I1,I2)=>`_==Int_`(`_%Int_`(I2,I1),#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5), org.kframework.attributes.Location(Location(1439,8,1439,58)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI1:SortInt{} + ),\and{R} ( + \in{SortInt{}, R} ( + X1:SortInt{}, + VarI2:SortInt{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'dividesInt'UndsUnds'INT-COMMON'Unds'Bool'Unds'Int'Unds'Int{}(X0:SortInt{},X1:SortInt{}), + \and{SortBool{}} ( + Lbl'UndsEqlsEqls'Int'Unds'{}(Lbl'UndsPerc'Int'Unds'{}(VarI2:SortInt{},VarI1:SortInt{}),\dv{SortInt{}}("0")), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("fd8facae0061fe5bc5c406f7ad2ed5d8d21960bf1118c9b240451253064dadb5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1439,8,1439,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_impliesBool_`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba), org.kframework.attributes.Location(Location(1157,8,1157,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'impliesBool'Unds'{}(VarB:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + LblnotBool'Unds'{}(VarB:SortBool{}), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("93b8d798abd6d9999e0e733384ad161e9a0bd2f074623a742afdc63964380aba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1157,8,1157,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_impliesBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba), org.kframework.attributes.Location(Location(1156,8,1156,39)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'impliesBool'Unds'{}(Var'Unds'Gen0:SortBool{},\dv{SortBool{}}("true")), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2b4994db7b40b72dc09ac8d5d036263b215c37d45f45d764251d8b607a7592ba"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1156,8,1156,39)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_impliesBool_`(#token("false","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e), org.kframework.attributes.Location(Location(1155,8,1155,40)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("false") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + Var'Unds'Gen0:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'impliesBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("55bb5c83c9563c712537b95401c0a5c88255fd7cdbd18b2d4358c54aee80660e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1155,8,1155,40)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_impliesBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d), org.kframework.attributes.Location(Location(1154,8,1154,36)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'impliesBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("da818c43c21c5fb2cced7e02a74b6b4191d323de2967a671b961ad28550f3c7d"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1154,8,1154,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_modInt_`(I1,I2)=>`_%Int_`(`_+Int_`(`_%Int_`(I1,`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)),`absInt(_)_INT-COMMON_Int_Int`(I2)) requires `_=/=Int_`(I2,#token("0","Int")) ensures #token("true","Bool") [UNIQUE_ID(44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4), concrete, org.kframework.attributes.Location(Location(1430,5,1433,23)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol]), simplification] + axiom{R} \implies{R} ( + \equals{SortBool{},R}( + Lbl'UndsEqlsSlshEqls'Int'Unds'{}(VarI2:SortInt{},\dv{SortInt{}}("0")), + \dv{SortBool{}}("true")), + \equals{SortInt{},R} ( + Lbl'Unds'modInt'Unds'{}(VarI1:SortInt{},VarI2:SortInt{}), + \and{SortInt{}} ( + Lbl'UndsPerc'Int'Unds'{}(Lbl'UndsPlus'Int'Unds'{}(Lbl'UndsPerc'Int'Unds'{}(VarI1:SortInt{},LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})),LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})),LblabsInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(VarI2:SortInt{})), + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("44257f63a99a0583c2d10058edbff90118966e30914b3a637b8315212c681bc4"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1430,5,1433,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_orBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff), org.kframework.attributes.Location(Location(1147,8,1147,32)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'orBool'Unds'{}(VarB:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("a5bb27ab54700cb845d17b12e0b0a4cbd5c8944272bcbe0d15ccc0b44d0049ff"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1147,8,1147,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_orBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e), org.kframework.attributes.Location(Location(1145,8,1145,34)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'orBool'Unds'{}(Var'Unds'Gen0:SortBool{},\dv{SortBool{}}("true")), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("942af273100b5a3c1fb3d0c8cc92b0bf845a7b34444c5a6c35b7d3fe72bef48e"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1145,8,1145,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_orBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b), org.kframework.attributes.Location(Location(1146,8,1146,32)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("false") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'orBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("991a3290bc7b6dca75d676a72a848ec6b2bd2827fb0e9626252aa1507394ca1b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1146,8,1146,32)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_orBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2), org.kframework.attributes.Location(Location(1144,8,1144,34)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + Var'Unds'Gen0:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'orBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("71744528cdad83bc729990d3af3b544d27b09630b2615ca707dd2fc6ec93e7c2"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1144,8,1144,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_orElseBool_`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b), org.kframework.attributes.Location(Location(1152,8,1152,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'orElseBool'Unds'{}(VarK:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + VarK:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("13cf42d440f9a7a360a8136ee4b35ae7b99501f515322d214c3b866691f4713b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1152,8,1152,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_orElseBool_`(_Gen0,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158), org.kframework.attributes.Location(Location(1150,8,1150,33)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'orElseBool'Unds'{}(Var'Unds'Gen0:SortBool{},\dv{SortBool{}}("true")), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2459cad4fbb946a5c7f71565601afeeec79f05f41497b1f7ef547578c88f3158"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1150,8,1150,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_orElseBool_`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf), org.kframework.attributes.Location(Location(1151,8,1151,37)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("false") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarK:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'orElseBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarK:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("eb8c85dac19a5951f694b65269c2b17c80d6d126d6a367958e4a5d736a880ecf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1151,8,1151,37)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_orElseBool_`(#token("true","Bool"),_Gen0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6), org.kframework.attributes.Location(Location(1149,8,1149,33)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + Var'Unds'Gen0:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'orElseBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("354bd0860c7f38b59e285c935fd2ea553ebddbabb4973342ad25f0dac6ea7bf6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1149,8,1149,33)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_xorBool_`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f), org.kframework.attributes.Location(Location(1142,8,1142,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + VarB:SortBool{} + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'xorBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("9a6d91cd75cd777b0d4db536b3e4b20578e74fe650e644b55294da95fd2dba7f"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1142,8,1142,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_xorBool_`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa), org.kframework.attributes.Location(Location(1141,8,1141,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol]), simplification] + axiom{R} \implies{R} ( + \top{R}(), + \equals{SortBool{},R} ( + Lbl'Unds'xorBool'Unds'{}(VarB:SortBool{},\dv{SortBool{}}("false")), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("69f518203376930fb76ce51df5dd0c6c81d19f71eba3a1852afa5301d02eb4fa"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1141,8,1141,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), simplification{}()] + +// rule `_xorBool_`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf), org.kframework.attributes.Location(Location(1140,8,1140,38)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("false") + ),\and{R} ( + \in{SortBool{}, R} ( + X1:SortBool{}, + VarB:SortBool{} + ), + \top{R} () + ))), + \equals{SortBool{},R} ( + Lbl'Unds'xorBool'Unds'{}(X0:SortBool{},X1:SortBool{}), + \and{SortBool{}} ( + VarB:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("73513655c09a595907ab9d26d67e27f01d14a3435743b77000c02d10f35c05bf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1140,8,1140,38)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `_|Set__SET_Set_Set_Set`(S1,S2)=>`_Set_`(S1,`Set:difference`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9), concrete, org.kframework.attributes.Location(Location(749,8,749,45)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortSet{}, R} ( + X0:SortSet{}, + VarS1:SortSet{} + ),\and{R} ( + \in{SortSet{}, R} ( + X1:SortSet{}, + VarS2:SortSet{} + ), + \top{R} () + ))), + \equals{SortSet{},R} ( + Lbl'UndsPipe'Set'UndsUnds'SET'Unds'Set'Unds'Set'Unds'Set{}(X0:SortSet{},X1:SortSet{}), + \and{SortSet{}} ( + Lbl'Unds'Set'Unds'{}(VarS1:SortSet{},LblSet'Coln'difference{}(VarS2:SortSet{},VarS1:SortSet{})), + \top{SortSet{}}()))) + [UNIQUE'Unds'ID{}("c384edb8f3875244a593dda6163c3dee1bce5485e4e1848892aebc2bab67d2e9"), concrete{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(749,8,749,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_modInt_`(`_>>Int_`(I,IDX),`_<I requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b), org.kframework.attributes.Location(Location(1442,8,1442,28)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI:SortInt{} + ), + \top{R} () + )), + \equals{SortInt{},R} ( + LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(X0:SortInt{}), + \and{SortInt{}} ( + VarI:SortInt{}, + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("cf2cb8f038b4bdc4edb1334a3b8ced9cd296a7af43f0a1916e082a4e1aefa08b"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1442,8,1442,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule getGeneratedCounterCell(``(_Gen0,_Gen1,_Gen2,Cell))=>Cell requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(551c4ed64b8c5b44b3ddddd4b2894e61a7de367903c9212cbae5f0decc721c4d)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortGeneratedTopCell{}, R} ( + X0:SortGeneratedTopCell{}, + Lbl'-LT-'generatedTop'-GT-'{}(Var'Unds'Gen0:SortKCell{},Var'Unds'Gen1:SortListCell{},Var'Unds'Gen2:SortCounterCell{},VarCell:SortGeneratedCounterCell{}) + ), + \top{R} () + )), + \equals{SortGeneratedCounterCell{},R} ( + LblgetGeneratedCounterCell{}(X0:SortGeneratedTopCell{}), + \and{SortGeneratedCounterCell{}} ( + VarCell:SortGeneratedCounterCell{}, + \top{SortGeneratedCounterCell{}}()))) + [UNIQUE'Unds'ID{}("551c4ed64b8c5b44b3ddddd4b2894e61a7de367903c9212cbae5f0decc721c4d")] + +// rule initCounterCell(.KList)=>``(#token("100000","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3f473c5a9052e536946a203bdcc2461ea3f2fe9bce42e765155e589e2bce1008), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortCounterCell{},R} ( + LblinitCounterCell{}(), + \and{SortCounterCell{}} ( + Lbl'-LT-'counter'-GT-'{}(\dv{SortInt{}}("100000")), + \top{SortCounterCell{}}()))) + [UNIQUE'Unds'ID{}("3f473c5a9052e536946a203bdcc2461ea3f2fe9bce42e765155e589e2bce1008")] + +// rule initGeneratedCounterCell(.KList)=>``(#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5de11f6b50c4684c0e05b773f809d756f4ce9c03a4f24e23a9cddaf3fa31f553), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortGeneratedCounterCell{},R} ( + LblinitGeneratedCounterCell{}(), + \and{SortGeneratedCounterCell{}} ( + Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")), + \top{SortGeneratedCounterCell{}}()))) + [UNIQUE'Unds'ID{}("5de11f6b50c4684c0e05b773f809d756f4ce9c03a4f24e23a9cddaf3fa31f553")] + +// rule initGeneratedTopCell(.KList)=>``(initKCell(.KList),initListCell(.KList),initCounterCell(.KList),initGeneratedCounterCell(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(a3e06be0d79d5e0f6f63ece82cf2eba3333daa155d64bd998caf1c3e6dd88544), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortGeneratedTopCell{},R} ( + LblinitGeneratedTopCell{}(), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(LblinitKCell{}(),LblinitListCell{}(),LblinitCounterCell{}(),LblinitGeneratedCounterCell{}()), + \top{SortGeneratedTopCell{}}()))) + [UNIQUE'Unds'ID{}("a3e06be0d79d5e0f6f63ece82cf2eba3333daa155d64bd998caf1c3e6dd88544")] + +// rule initKCell(.KList)=>``(inj{Pgm,KItem}(`foo()_TEST_Pgm`(.KList))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(46d7ca6dac9a23435534d09fe03ae3fdcfa7ba8be7d2d3a17713fa4640c712d3), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortKCell{},R} ( + LblinitKCell{}(), + \and{SortKCell{}} ( + Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortPgm{}, SortKItem{}}(Lblfoo'LParRParUnds'TEST'Unds'Pgm{}()),dotk{}())), + \top{SortKCell{}}()))) + [UNIQUE'Unds'ID{}("46d7ca6dac9a23435534d09fe03ae3fdcfa7ba8be7d2d3a17713fa4640c712d3")] + +// rule initListCell(.KList)=>``(`baz(_)_TEST_KItem_List`(`_List_`(`ListItem`(inj{Int,KItem}(#token("3","Int"))),`ListItem`(inj{Int,KItem}(#token("4","Int")))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(efac35c3165c0b6506fa55be060db3788ebb3c3426067d3589656b0335a73241), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortListCell{},R} ( + LblinitListCell{}(), + \and{SortListCell{}} ( + Lbl'-LT-'list'-GT-'{}(Lblbaz'LParUndsRParUnds'TEST'Unds'KItem'Unds'List{}(Lbl'Unds'List'Unds'{}(LblListItem{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("3"))),LblListItem{}(inj{SortInt{}, SortKItem{}}(\dv{SortInt{}}("4")))))), + \top{SortListCell{}}()))) + [UNIQUE'Unds'ID{}("efac35c3165c0b6506fa55be060db3788ebb3c3426067d3589656b0335a73241")] + +// rule isBool(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(495da551d13b205c8648618471ccfca028707f98eff21e6b11d591515ed6f29a), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortBool{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen1:SortBool{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisBool{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("495da551d13b205c8648618471ccfca028707f98eff21e6b11d591515ed6f29a"), owise{}()] + +// rule isBool(inj{Bool,KItem}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(dadad716b2f6a82fa4b2cc8f903a1b8f1f6e8cfa63f18b72a7cb35110bdcff77)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBool{}, SortKItem{}}(VarBool:SortBool{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisBool{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("dadad716b2f6a82fa4b2cc8f903a1b8f1f6e8cfa63f18b72a7cb35110bdcff77")] + +// rule isCounterCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2bbe2884c93fff45740c8acb41aed03c051c94c5af24329a32aa5d0c2af814fa), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortCounterCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCell{}, SortKItem{}}(Var'Unds'Gen0:SortCounterCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisCounterCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2bbe2884c93fff45740c8acb41aed03c051c94c5af24329a32aa5d0c2af814fa"), owise{}()] + +// rule isCounterCell(inj{CounterCell,KItem}(CounterCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e5650ff7b70e4300ed1f267030d45b5ea020807c57d192fbec50f728c8b29134)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCell{}, SortKItem{}}(VarCounterCell:SortCounterCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisCounterCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("e5650ff7b70e4300ed1f267030d45b5ea020807c57d192fbec50f728c8b29134")] + +// rule isCounterCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(61480dd6a4d15022a136211e59e20ebcac858e18d9326e86f873251bc6c6908d), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortCounterCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortCounterCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisCounterCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("61480dd6a4d15022a136211e59e20ebcac858e18d9326e86f873251bc6c6908d"), owise{}()] + +// rule isCounterCellOpt(inj{CounterCellOpt,KItem}(CounterCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(dec0ed9994706e49a2992e47083ccb95d6708944caab5f9f65def5354bb271c9)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCellOpt{}, SortKItem{}}(VarCounterCellOpt:SortCounterCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisCounterCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("dec0ed9994706e49a2992e47083ccb95d6708944caab5f9f65def5354bb271c9")] + +// rule isGeneratedCounterCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(b0c8eb86594a387398bf96f2dbf773cff29d14b8a45c5f6701f205bf3d2f33ba), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortGeneratedCounterCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedCounterCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisGeneratedCounterCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("b0c8eb86594a387398bf96f2dbf773cff29d14b8a45c5f6701f205bf3d2f33ba"), owise{}()] + +// rule isGeneratedCounterCell(inj{GeneratedCounterCell,KItem}(GeneratedCounterCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f7b6a3dbee5a80d5eeba727f40009876995660d4052a45fc50c55f88c5fc1a7c)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(VarGeneratedCounterCell:SortGeneratedCounterCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisGeneratedCounterCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("f7b6a3dbee5a80d5eeba727f40009876995660d4052a45fc50c55f88c5fc1a7c")] + +// rule isGeneratedTopCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ccb9226d9e6c0e476485f098ef162c6c2206ed3af1d8336ea3ae859b86bc4a8b), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortGeneratedTopCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(Var'Unds'Gen1:SortGeneratedTopCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisGeneratedTopCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ccb9226d9e6c0e476485f098ef162c6c2206ed3af1d8336ea3ae859b86bc4a8b"), owise{}()] + +// rule isGeneratedTopCell(inj{GeneratedTopCell,KItem}(GeneratedTopCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3bcf423225700e329d0533cfd806eb9bab91f9d8de0979c8d8e381fe5d076bb2)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(VarGeneratedTopCell:SortGeneratedTopCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisGeneratedTopCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("3bcf423225700e329d0533cfd806eb9bab91f9d8de0979c8d8e381fe5d076bb2")] + +// rule isGeneratedTopCellFragment(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(98049f5819962c7ee2b01436957b6cf8460b106979fa2c24f4c606bbf6cb1592), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortGeneratedTopCellFragment{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(Var'Unds'Gen0:SortGeneratedTopCellFragment{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisGeneratedTopCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("98049f5819962c7ee2b01436957b6cf8460b106979fa2c24f4c606bbf6cb1592"), owise{}()] + +// rule isGeneratedTopCellFragment(inj{GeneratedTopCellFragment,KItem}(GeneratedTopCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(559f2cdc0ab425bb065cc3174f4a1af4d9ca834f762a814cf3dfbf9a9d7f8271)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(VarGeneratedTopCellFragment:SortGeneratedTopCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisGeneratedTopCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("559f2cdc0ab425bb065cc3174f4a1af4d9ca834f762a814cf3dfbf9a9d7f8271")] + +// rule isInt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(105572a4ac107eeb518b37c4d6ed3e28732b83afb0ba085d02d339c4fc2140a0), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortInt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortInt{}, SortKItem{}}(Var'Unds'Gen1:SortInt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisInt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("105572a4ac107eeb518b37c4d6ed3e28732b83afb0ba085d02d339c4fc2140a0"), owise{}()] + +// rule isInt(inj{Int,KItem}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(92664aa821c8898ff16b4e72ad0bdf363f755c7660d28dcb69c129a2c94bc6b5)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortInt{}, SortKItem{}}(VarInt:SortInt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisInt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("92664aa821c8898ff16b4e72ad0bdf363f755c7660d28dcb69c129a2c94bc6b5")] + +// rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(16ff77cff0ef50026a8b3f4614b87bda465701918596b7ad2280baffff56f847)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisK{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("16ff77cff0ef50026a8b3f4614b87bda465701918596b7ad2280baffff56f847")] + +// rule isKCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d30be57718b4b3745eaf2e99f875cfec7d5be2ff76bacde8a89bd4ab659d857f), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortKCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCell{}, SortKItem{}}(Var'Unds'Gen1:SortKCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisKCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("d30be57718b4b3745eaf2e99f875cfec7d5be2ff76bacde8a89bd4ab659d857f"), owise{}()] + +// rule isKCell(inj{KCell,KItem}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2695222b1238f711f8a356c0a1bc0ac418d7bd78fd3282e7c60882e2631a46df)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCell{}, SortKItem{}}(VarKCell:SortKCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisKCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2695222b1238f711f8a356c0a1bc0ac418d7bd78fd3282e7c60882e2631a46df")] + +// rule isKCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a3f84195242c98b432c7c63a4189f4276cc3189445c5cf37ce08d9a6547b1f7), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortKCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortKCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisKCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("9a3f84195242c98b432c7c63a4189f4276cc3189445c5cf37ce08d9a6547b1f7"), owise{}()] + +// rule isKCellOpt(inj{KCellOpt,KItem}(KCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(1516473b1e153a368c273997543a4378ad451e5e828db8e289f4447f7e5228a5)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCellOpt{}, SortKItem{}}(VarKCellOpt:SortKCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisKCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("1516473b1e153a368c273997543a4378ad451e5e828db8e289f4447f7e5228a5")] + +// rule isKConfigVar(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f68a616e301c35586f68e97b729ae274278c3ef8fe6634711cfd3e1746bc0bc2), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortKConfigVar{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKConfigVar{}, SortKItem{}}(Var'Unds'Gen1:SortKConfigVar{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisKConfigVar{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("f68a616e301c35586f68e97b729ae274278c3ef8fe6634711cfd3e1746bc0bc2"), owise{}()] + +// rule isKConfigVar(inj{KConfigVar,KItem}(KConfigVar))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(0ef0a00bb321f2c2a62a3239327de70ecb8e907a950cd20034c46b84e040ebcd)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKConfigVar{}, SortKItem{}}(VarKConfigVar:SortKConfigVar{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisKConfigVar{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("0ef0a00bb321f2c2a62a3239327de70ecb8e907a950cd20034c46b84e040ebcd")] + +// rule isKItem(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(83812b6b9e31a764d66d89fd1c7e65b9b162d52c5aebfe99b1536e200a9590c2), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortKItem{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(Var'Unds'Gen1:SortKItem{},dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisKItem{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("83812b6b9e31a764d66d89fd1c7e65b9b162d52c5aebfe99b1536e200a9590c2"), owise{}()] + +// rule isKItem(KItem)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ed3c25a7dab5e5fbc101589e2fa74ac91aa107f051d22a01378222d08643373c)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(VarKItem:SortKItem{},dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisKItem{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ed3c25a7dab5e5fbc101589e2fa74ac91aa107f051d22a01378222d08643373c")] + +// rule isList(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9a9489adcf0279eca74c012bb1130bb9d30372cfbebc8e4ab4b173656c4d6613), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortList{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen1:SortList{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisList{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("9a9489adcf0279eca74c012bb1130bb9d30372cfbebc8e4ab4b173656c4d6613"), owise{}()] + +// rule isList(inj{List,KItem}(List))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7d4dddf5bbdb61cfd11fb9be1071be7bd551cf186607cf6f493cfade3221c446)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortList{}, SortKItem{}}(VarList:SortList{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisList{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("7d4dddf5bbdb61cfd11fb9be1071be7bd551cf186607cf6f493cfade3221c446")] + +// rule isListCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f2ccbb7fe8f4f49807fcd1aafef05a0f06880dd57b60e929a58406246c4173b6), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortListCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCell{}, SortKItem{}}(Var'Unds'Gen1:SortListCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisListCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("f2ccbb7fe8f4f49807fcd1aafef05a0f06880dd57b60e929a58406246c4173b6"), owise{}()] + +// rule isListCell(inj{ListCell,KItem}(ListCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(b1327588ea0c347b202e8edeaf83c9f8f613ff179d422dfbc7c81fa8a2a5295c)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCell{}, SortKItem{}}(VarListCell:SortListCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisListCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("b1327588ea0c347b202e8edeaf83c9f8f613ff179d422dfbc7c81fa8a2a5295c")] + +// rule isListCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ecb0807e0d6a1a9a32c06809343058392ece37316d3a275c147f577320353899), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortListCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCellOpt{}, SortKItem{}}(Var'Unds'Gen1:SortListCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisListCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ecb0807e0d6a1a9a32c06809343058392ece37316d3a275c147f577320353899"), owise{}()] + +// rule isListCellOpt(inj{ListCellOpt,KItem}(ListCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(8cbb7bd9ec97937374b16b645664a1d10dfdbb8000eb832fbeb3b7130b777279)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCellOpt{}, SortKItem{}}(VarListCellOpt:SortListCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisListCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("8cbb7bd9ec97937374b16b645664a1d10dfdbb8000eb832fbeb3b7130b777279")] + +// rule isMap(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(6f30a2087d0b19640df005437bc3f4665f41282666a72821b17b16c99ed5afee), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortMap{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMap{}, SortKItem{}}(Var'Unds'Gen0:SortMap{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisMap{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("6f30a2087d0b19640df005437bc3f4665f41282666a72821b17b16c99ed5afee"), owise{}()] + +// rule isMap(inj{Map,KItem}(Map))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4879c0fcf6b7d7f3d6b751e4f460f8dced005a44ae5ff600cffcea784cf58795)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMap{}, SortKItem{}}(VarMap:SortMap{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisMap{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("4879c0fcf6b7d7f3d6b751e4f460f8dced005a44ae5ff600cffcea784cf58795")] + +// rule isPgm(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d81e24a5fb48fd63fad83552f4be2f353fc339daa0f1287ac210fda817b975c8), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortPgm{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortPgm{}, SortKItem{}}(Var'Unds'Gen1:SortPgm{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisPgm{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("d81e24a5fb48fd63fad83552f4be2f353fc339daa0f1287ac210fda817b975c8"), owise{}()] + +// rule isPgm(inj{Pgm,KItem}(Pgm))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ab1ce0ad25ba45a63671fdb97f4420e1f04f944e98383fcf5e38be330aa4a7d7)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortPgm{}, SortKItem{}}(VarPgm:SortPgm{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisPgm{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ab1ce0ad25ba45a63671fdb97f4420e1f04f944e98383fcf5e38be330aa4a7d7")] + +// rule isSet(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2b5aadccd9b89faba72816867187d48d279d8c27c8bda1a1b3b0658bd82bb783), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortSet{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortSet{}, SortKItem{}}(Var'Unds'Gen0:SortSet{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisSet{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("2b5aadccd9b89faba72816867187d48d279d8c27c8bda1a1b3b0658bd82bb783"), owise{}()] + +// rule isSet(inj{Set,KItem}(Set))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f205bc460bdb728b4c3458643699be30d519db4d8b13e80e2c27082b9e846e80)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortSet{}, SortKItem{}}(VarSet:SortSet{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisSet{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("f205bc460bdb728b4c3458643699be30d519db4d8b13e80e2c27082b9e846e80")] + +// rule ite{K}(C,B1,_Gen0)=>B1 requires C ensures #token("true","Bool") [UNIQUE_ID(1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0), org.kframework.attributes.Location(Location(2318,8,2318,59)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \equals{SortBool{},R}( + VarC:SortBool{}, + \dv{SortBool{}}("true")), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + VarC:SortBool{} + ),\and{R} ( + \in{SortK{}, R} ( + X1:SortK{}, + VarB1:SortK{} + ),\and{R} ( + \in{SortK{}, R} ( + X2:SortK{}, + Var'Unds'Gen0:SortK{} + ), + \top{R} () + )))), + \equals{SortK{},R} ( + Lblite{SortK{}}(X0:SortBool{},X1:SortK{},X2:SortK{}), + \and{SortK{}} ( + VarB1:SortK{}, + \top{SortK{}}()))) + [UNIQUE'Unds'ID{}("1ff8f4d71e4c13084eed473b08740da83c4cc7f1875d340d86dc72124c48b4a0"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2318,8,2318,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule ite{K}(C,_Gen0,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [UNIQUE_ID(2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5), org.kframework.attributes.Location(Location(2319,8,2319,67)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \equals{SortBool{},R}( + LblnotBool'Unds'{}(VarC:SortBool{}), + \dv{SortBool{}}("true")), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + VarC:SortBool{} + ),\and{R} ( + \in{SortK{}, R} ( + X1:SortK{}, + Var'Unds'Gen0:SortK{} + ),\and{R} ( + \in{SortK{}, R} ( + X2:SortK{}, + VarB2:SortK{} + ), + \top{R} () + )))), + \equals{SortK{},R} ( + Lblite{SortK{}}(X0:SortBool{},X1:SortK{},X2:SortK{}), + \and{SortK{}} ( + VarB2:SortK{}, + \top{SortK{}}()))) + [UNIQUE'Unds'ID{}("2f3f58a93926913fc5ca147dfd8d3d612508bc8ff67412ef10935df7c09554d5"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(2319,8,2319,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I1 requires `_<=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6), org.kframework.attributes.Location(Location(1435,8,1435,57)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \equals{SortBool{},R}( + Lbl'Unds-LT-Eqls'Int'Unds'{}(VarI1:SortInt{},VarI2:SortInt{}), + \dv{SortBool{}}("true")), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI1:SortInt{} + ),\and{R} ( + \in{SortInt{}, R} ( + X1:SortInt{}, + VarI2:SortInt{} + ), + \top{R} () + ))), + \equals{SortInt{},R} ( + LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(X0:SortInt{},X1:SortInt{}), + \and{SortInt{}} ( + VarI1:SortInt{}, + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("fb09b6acc4366cb77203e07c4efe8a9cf304e1bac9fb0664deea05d3eb9a80c6"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1435,8,1435,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I2 requires `_>=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3), org.kframework.attributes.Location(Location(1436,8,1436,57)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [klabel(#ruleRequires), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \equals{SortBool{},R}( + Lbl'Unds-GT-Eqls'Int'Unds'{}(VarI1:SortInt{},VarI2:SortInt{}), + \dv{SortBool{}}("true")), + \and{R} ( + \in{SortInt{}, R} ( + X0:SortInt{}, + VarI1:SortInt{} + ),\and{R} ( + \in{SortInt{}, R} ( + X1:SortInt{}, + VarI2:SortInt{} + ), + \top{R} () + ))), + \equals{SortInt{},R} ( + LblminInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int{}(X0:SortInt{},X1:SortInt{}), + \and{SortInt{}} ( + VarI2:SortInt{}, + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1436,8,1436,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415), org.kframework.attributes.Location(Location(1128,8,1128,29)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("false") + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblnotBool'Unds'{}(X0:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("17ebc68421572b8ebe609c068fb49cbb6cbbe3246e2142257ad8befdda38f415"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1128,8,1128,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c), org.kframework.attributes.Location(Location(1127,8,1127,29)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortBool{}, R} ( + X0:SortBool{}, + \dv{SortBool{}}("true") + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblnotBool'Unds'{}(X0:SortBool{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("53fc758ece1ff16581673016dfacc556cc30fcf6b3c35b586f001d76a1f9336c"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1127,8,1127,29)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `project:Bool`(inj{Bool,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5872f0d5b8131216db7bc41e2c3a423e55f4b8581589fcbd1bf93b2ca6862d54), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBool{}, SortKItem{}}(VarK:SortBool{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + Lblproject'Coln'Bool{}(X0:SortK{}), + \and{SortBool{}} ( + VarK:SortBool{}, + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("5872f0d5b8131216db7bc41e2c3a423e55f4b8581589fcbd1bf93b2ca6862d54")] + +// rule `project:CounterCell`(inj{CounterCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(9be273a25ebb910a9ba249ad071846e4d06ab1549ebb7c2ed65173db0d6e653b), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCell{}, SortKItem{}}(VarK:SortCounterCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortCounterCell{},R} ( + Lblproject'Coln'CounterCell{}(X0:SortK{}), + \and{SortCounterCell{}} ( + VarK:SortCounterCell{}, + \top{SortCounterCell{}}()))) + [UNIQUE'Unds'ID{}("9be273a25ebb910a9ba249ad071846e4d06ab1549ebb7c2ed65173db0d6e653b")] + +// rule `project:CounterCellOpt`(inj{CounterCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(24dd9c230ed8564926800041082534dd3a3ec38d418aca6c22a038dbccd35be1), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortCounterCellOpt{}, SortKItem{}}(VarK:SortCounterCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortCounterCellOpt{},R} ( + Lblproject'Coln'CounterCellOpt{}(X0:SortK{}), + \and{SortCounterCellOpt{}} ( + VarK:SortCounterCellOpt{}, + \top{SortCounterCellOpt{}}()))) + [UNIQUE'Unds'ID{}("24dd9c230ed8564926800041082534dd3a3ec38d418aca6c22a038dbccd35be1")] + +// rule `project:GeneratedCounterCell`(inj{GeneratedCounterCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(63453db9d9aa121b63bb877e2fa4998d399ef82d2a1e4b90f87a32ba55401217), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(VarK:SortGeneratedCounterCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortGeneratedCounterCell{},R} ( + Lblproject'Coln'GeneratedCounterCell{}(X0:SortK{}), + \and{SortGeneratedCounterCell{}} ( + VarK:SortGeneratedCounterCell{}, + \top{SortGeneratedCounterCell{}}()))) + [UNIQUE'Unds'ID{}("63453db9d9aa121b63bb877e2fa4998d399ef82d2a1e4b90f87a32ba55401217")] + +// rule `project:GeneratedTopCell`(inj{GeneratedTopCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(b0fabd8c7c81fe08ebd569aff59747d357e441ae1fcd05d9d594d57e38e3d55e), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCell{}, SortKItem{}}(VarK:SortGeneratedTopCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortGeneratedTopCell{},R} ( + Lblproject'Coln'GeneratedTopCell{}(X0:SortK{}), + \and{SortGeneratedTopCell{}} ( + VarK:SortGeneratedTopCell{}, + \top{SortGeneratedTopCell{}}()))) + [UNIQUE'Unds'ID{}("b0fabd8c7c81fe08ebd569aff59747d357e441ae1fcd05d9d594d57e38e3d55e")] + +// rule `project:GeneratedTopCellFragment`(inj{GeneratedTopCellFragment,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2084fac322aa142a07f881814b8a286bf62d5c6d05777b7aa715ccc534cf9a42), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(VarK:SortGeneratedTopCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortGeneratedTopCellFragment{},R} ( + Lblproject'Coln'GeneratedTopCellFragment{}(X0:SortK{}), + \and{SortGeneratedTopCellFragment{}} ( + VarK:SortGeneratedTopCellFragment{}, + \top{SortGeneratedTopCellFragment{}}()))) + [UNIQUE'Unds'ID{}("2084fac322aa142a07f881814b8a286bf62d5c6d05777b7aa715ccc534cf9a42")] + +// rule `project:Int`(inj{Int,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f316b871091516c401f1d2382cc5f66322602b782c7b01e1aeb6c2ddab50e24b), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortInt{}, SortKItem{}}(VarK:SortInt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortInt{},R} ( + Lblproject'Coln'Int{}(X0:SortK{}), + \and{SortInt{}} ( + VarK:SortInt{}, + \top{SortInt{}}()))) + [UNIQUE'Unds'ID{}("f316b871091516c401f1d2382cc5f66322602b782c7b01e1aeb6c2ddab50e24b")] + +// rule `project:K`(K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(25b529ddcefd25ef63f99a62040145ef27638e7679ea9202218fe14be98dff3a), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + )), + \equals{SortK{},R} ( + Lblproject'Coln'K{}(X0:SortK{}), + \and{SortK{}} ( + VarK:SortK{}, + \top{SortK{}}()))) + [UNIQUE'Unds'ID{}("25b529ddcefd25ef63f99a62040145ef27638e7679ea9202218fe14be98dff3a")] + +// rule `project:KCell`(inj{KCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(894c13c4c410f11e35bc3781505aeddde4ff400ddda1daf8b35259dbf0de9a24), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCell{}, SortKItem{}}(VarK:SortKCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortKCell{},R} ( + Lblproject'Coln'KCell{}(X0:SortK{}), + \and{SortKCell{}} ( + VarK:SortKCell{}, + \top{SortKCell{}}()))) + [UNIQUE'Unds'ID{}("894c13c4c410f11e35bc3781505aeddde4ff400ddda1daf8b35259dbf0de9a24")] + +// rule `project:KCellOpt`(inj{KCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f684dd78d97feadf0cbcb3cbb8892e0842f137c7b29a904cb2f3fc9755b29b30), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKCellOpt{}, SortKItem{}}(VarK:SortKCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortKCellOpt{},R} ( + Lblproject'Coln'KCellOpt{}(X0:SortK{}), + \and{SortKCellOpt{}} ( + VarK:SortKCellOpt{}, + \top{SortKCellOpt{}}()))) + [UNIQUE'Unds'ID{}("f684dd78d97feadf0cbcb3cbb8892e0842f137c7b29a904cb2f3fc9755b29b30")] + +// rule `project:KItem`(K)=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(1242e49c17638c9a66a35e3bb8c237288f7e9aa9a6499101e8cdc55be320cd29), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(VarK:SortKItem{},dotk{}()) + ), + \top{R} () + )), + \equals{SortKItem{},R} ( + Lblproject'Coln'KItem{}(X0:SortK{}), + \and{SortKItem{}} ( + VarK:SortKItem{}, + \top{SortKItem{}}()))) + [UNIQUE'Unds'ID{}("1242e49c17638c9a66a35e3bb8c237288f7e9aa9a6499101e8cdc55be320cd29")] + +// rule `project:List`(inj{List,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2b75eac5a59779d336e6cf9632bf9ba7d67286f322e753108b34e62f2443efe5), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortList{}, SortKItem{}}(VarK:SortList{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortList{},R} ( + Lblproject'Coln'List{}(X0:SortK{}), + \and{SortList{}} ( + VarK:SortList{}, + \top{SortList{}}()))) + [UNIQUE'Unds'ID{}("2b75eac5a59779d336e6cf9632bf9ba7d67286f322e753108b34e62f2443efe5")] + +// rule `project:ListCell`(inj{ListCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(24b644032121515b619d0259c1d130450411e09ae1f2358b26a2968f877f7866), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCell{}, SortKItem{}}(VarK:SortListCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortListCell{},R} ( + Lblproject'Coln'ListCell{}(X0:SortK{}), + \and{SortListCell{}} ( + VarK:SortListCell{}, + \top{SortListCell{}}()))) + [UNIQUE'Unds'ID{}("24b644032121515b619d0259c1d130450411e09ae1f2358b26a2968f877f7866")] + +// rule `project:ListCellOpt`(inj{ListCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(7e25d1215e21bc8a2d69b13feb4d7cd1fce1be9fd78c6cab77d933d4ccc952f3), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortListCellOpt{}, SortKItem{}}(VarK:SortListCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortListCellOpt{},R} ( + Lblproject'Coln'ListCellOpt{}(X0:SortK{}), + \and{SortListCellOpt{}} ( + VarK:SortListCellOpt{}, + \top{SortListCellOpt{}}()))) + [UNIQUE'Unds'ID{}("7e25d1215e21bc8a2d69b13feb4d7cd1fce1be9fd78c6cab77d933d4ccc952f3")] + +// rule `project:Map`(inj{Map,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(031237d4aae58d86914d6370d37ccd15f4738378ed780333c59cc81b4f7bc598), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortMap{}, SortKItem{}}(VarK:SortMap{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortMap{},R} ( + Lblproject'Coln'Map{}(X0:SortK{}), + \and{SortMap{}} ( + VarK:SortMap{}, + \top{SortMap{}}()))) + [UNIQUE'Unds'ID{}("031237d4aae58d86914d6370d37ccd15f4738378ed780333c59cc81b4f7bc598")] + +// rule `project:Pgm`(inj{Pgm,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ddb4777eb97ab87ee0e1ea5bab55f10607991a4f447f275af1037d1b7c18329d), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortPgm{}, SortKItem{}}(VarK:SortPgm{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortPgm{},R} ( + Lblproject'Coln'Pgm{}(X0:SortK{}), + \and{SortPgm{}} ( + VarK:SortPgm{}, + \top{SortPgm{}}()))) + [UNIQUE'Unds'ID{}("ddb4777eb97ab87ee0e1ea5bab55f10607991a4f447f275af1037d1b7c18329d")] + +// rule `project:Set`(inj{Set,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(0e7f5070c993161786e314f7199d985afebac9e07b5c784f6f623780c60ce9d0), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortSet{}, SortKItem{}}(VarK:SortSet{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortSet{},R} ( + Lblproject'Coln'Set{}(X0:SortK{}), + \and{SortSet{}} ( + VarK:SortSet{}, + \top{SortSet{}}()))) + [UNIQUE'Unds'ID{}("0e7f5070c993161786e314f7199d985afebac9e07b5c784f6f623780c60ce9d0")] + +// rule pushList(K,L1)=>`_List_`(`ListItem`(K),L1) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf), org.kframework.attributes.Location(Location(954,8,954,54)), org.kframework.attributes.Source(Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [klabel(#ruleNoConditions), symbol])] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortKItem{}, R} ( + X0:SortKItem{}, + VarK:SortKItem{} + ),\and{R} ( + \in{SortList{}, R} ( + X1:SortList{}, + VarL1:SortList{} + ), + \top{R} () + ))), + \equals{SortList{},R} ( + LblpushList{}(X0:SortKItem{},X1:SortList{}), + \and{SortList{}} ( + Lbl'Unds'List'Unds'{}(LblListItem{}(VarK:SortKItem{}),VarL1:SortList{}), + \top{SortList{}}()))) + [UNIQUE'Unds'ID{}("f6967050cc4ec32c2d34d52f5577e09120f730420d2c5dc838cba81d04c57adf"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(954,8,954,54)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/kframework/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `signExtendBitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN)=>`_-Int_`(`_modInt_`(`_+Int_`(`bitRangeInt(_,_,_)_INT-COMMON_Int_Int_Int_Int`(I,IDX,LEN),`_<