From 7ab1decebbff0badaddc9d6505f0f4e9b1171aff Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Thu, 17 Oct 2024 17:02:19 -0300 Subject: [PATCH] Only emitting side_conditions if all occurrences of the same variable are equal (#1155) In this PR, we inverse the order in which we create the decision tree when a rule has a side condition. Previously, even when we had 2 or more variables with the same name having different values, the side condition decision trees were generated, and we only evaluated the variables matching after evaluating the side condition. After this PR, we inverse this order and evaluate the variables matching first and then the side condition. This issue was discovered in the context of side conditions proof events being emitted and being true but without ever being applied, as we have a mismatch in the variable names and values. This PR fixes: https://github.com/Pi-Squared-Inc/pi2/issues/2124 We added a regression test that reproduced this issue, and it's now fixed! --- .../backend/llvm/matching/Matrix.scala | 14 +- .../same-name-diff-value/transferFunds.in | 2 + .../transferFunds.proof.out.diff | 29 + test/proof/k-files/same-name-diff-value.k | 64 + test/proof/same-name-diff-value.kore | 3206 +++++++++++++++++ 5 files changed, 3308 insertions(+), 7 deletions(-) create mode 100644 test/input/same-name-diff-value/transferFunds.in create mode 100644 test/output/same-name-diff-value/transferFunds.proof.out.diff create mode 100644 test/proof/k-files/same-name-diff-value.k create mode 100644 test/proof/same-name-diff-value.kore diff --git a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala index 39fee871b..5f251cf3a 100644 --- a/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala +++ b/matching/src/main/scala/org/kframework/backend/llvm/matching/Matrix.scala @@ -766,12 +766,9 @@ class Matrix private ( Leaf(row.clause.action.ordinal, newVars) } // check that all occurrences of the same variable are equal - val nonlinearLeaf = nonlinearPairs.foldRight[DecisionTree](atomicLeaf)((e, dt) => - e._2.foldRight(dt)((os, dt2) => makeEquality(os._1._1, (os._1._2, os._2._2), dt2)) - ) - val sc = row.clause.action.scVars match { + val sc: DecisionTree = row.clause.action.scVars match { // if there is no side condition, continue - case None => nonlinearLeaf + case None => atomicLeaf case Some(cond) => val condVars = cond.map(v => (grouped(v).head._2, grouped(v).head._1.hookAtt)) val newO = SC(row.clause.action.ordinal) @@ -785,13 +782,16 @@ class Matrix private ( newO, "BOOL.Bool", 1, - immutable.Seq(("1", immutable.Seq(), nonlinearLeaf), ("0", immutable.Seq(), child)), + immutable.Seq(("1", immutable.Seq(), atomicLeaf), ("0", immutable.Seq(), child)), None ) ) } + val nonlinearLeaf = nonlinearPairs.foldRight[DecisionTree](sc)((e, dt) => + e._2.foldRight(dt)((os, dt2) => makeEquality(os._1._1, (os._1._2, os._2._2), dt2)) + ) // fill out the bindings for list range variables - val withRanges = row.clause.listRanges.foldRight(sc) { + val withRanges = row.clause.listRanges.foldRight(nonlinearLeaf) { case ((o @ Num(_, o2), hd, tl), dt) => Function( "hook_LIST_range_long", diff --git a/test/input/same-name-diff-value/transferFunds.in b/test/input/same-name-diff-value/transferFunds.in new file mode 100644 index 000000000..84870eee6 --- /dev/null +++ b/test/input/same-name-diff-value/transferFunds.in @@ -0,0 +1,2 @@ +LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM")),inj{SortOps{}, SortKItem{}}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),inj{SortOp{}, SortOps{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))))))) + diff --git a/test/output/same-name-diff-value/transferFunds.proof.out.diff b/test/output/same-name-diff-value/transferFunds.proof.out.diff new file mode 100644 index 000000000..32cf222d7 --- /dev/null +++ b/test/output/same-name-diff-value/transferFunds.proof.out.diff @@ -0,0 +1,29 @@ +version: 13 +hook: MAP.concat Lbl'Unds'Map'Unds'{} () + arg: kore[Lbl'Stop'Map{}()] + arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] +hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] +function: LblinitGeneratedTopCell{} () +rule: 231 1 + VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] +function: LblinitKCell{} (0) +rule: 232 1 + VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] +hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0) + arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))))] + arg: kore[\dv{SortKConfigVar{}}("$PGM")] +hook result: kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))] +function: Lblproject'Coln'Ops{} (0:0) +rule: 313 1 + VarK = kore[Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")))] +function: LblinitAccountsCell{} (1) +rule: 227 0 +function: LblinitGeneratedCounterCell{} (2) +rule: 230 0 +config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\dv{SortInt{}}("0"),\dv{SortInt{}}("5")),Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(Lbl'Stop'AccountCellMap{}()),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))] +rule: 191 4 + Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))] + VarACCT = kore[\dv{SortInt{}}("0")] + VarO = kore[Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1"))] + VarVALUE = kore[\dv{SortInt{}}("5")] +config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\dv{SortInt{}}("1"),\dv{SortInt{}}("0"),\dv{SortInt{}}("1")),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")),Lbl'-LT-'balance'-GT-'{}(\dv{SortInt{}}("5"))))),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))] diff --git a/test/proof/k-files/same-name-diff-value.k b/test/proof/k-files/same-name-diff-value.k new file mode 100644 index 000000000..36dffda39 --- /dev/null +++ b/test/proof/k-files/same-name-diff-value.k @@ -0,0 +1,64 @@ +module SAME-NAME-DIFF-VALUE + imports INT + imports K-EQUAL + imports BOOL + + configuration $PGM:Ops + + + 0 + 0 + + + + syntax Ops ::= Op ";" Ops [symbol(seq)] + | Op + + syntax Op ::= "#transferFunds" Int Int Int + | "#init" Int Int + + syntax NoOp ::= "#finish" + + + rule #init ACCT VALUE ; O:Op => O + + ( .Bag + => + + ACCT + VALUE + + ) + + + rule #transferFunds ACCT ACCT VALUE => .K ... + + ACCT + ORIGFROM + + requires VALUE <=Int ORIGFROM + + + rule #transferFunds ACCTFROM ACCTTO VALUE => .K ... + + ACCTFROM + ORIGFROM => ORIGFROM -Int VALUE + ... + + + ACCTTO + ORIGTO => ORIGTO +Int VALUE + ... + + requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM + [preserves-definedness] + + rule #transferFunds ACCTFROM _ACCTTO VALUE => .K ... + + ACCTFROM + ORIGFROM + ... + + requires VALUE >Int ORIGFROM + +endmodule \ No newline at end of file diff --git a/test/proof/same-name-diff-value.kore b/test/proof/same-name-diff-value.kore new file mode 100644 index 000000000..9902c0ed8 --- /dev/null +++ b/test/proof/same-name-diff-value.kore @@ -0,0 +1,3206 @@ +// RUN: %proof-interpreter +// RUN: %check-dir-proof-out +[topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.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 SAME-NAME-DIFF-VALUE + +// imports + import K [] + +// sorts + sort SortBalanceCell{} [] + sort SortAccountCellFragment{} [] + sort SortKCellOpt{} [] + sort SortAccountsCellOpt{} [] + sort SortAcctIDCellOpt{} [] + sort SortAccountsCellFragment{} [] + sort SortBalanceCellOpt{} [] + sort SortKConfigVar{} [hasDomainValues{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(40,3,40,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Set{}())] + sort SortOp{} [] + 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-sort SortAccountCellMap{} [concat{}(Lbl'Unds'AccountCellMap'Unds'{}()), element{}(LblAccountCellMapItem{}()), hook{}("MAP.Map"), unit{}(Lbl'Stop'AccountCellMap{}())] + sort SortGeneratedTopCellFragment{} [] + sort SortAcctIDCell{} [] + 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'List{}()), update{}(LblList'Coln'set{}())] + sort SortKCell{} [] + sort SortNoOp{} [] + sort SortGeneratedTopCell{} [] + sort SortGeneratedCounterCell{} [] + 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), unit{}(Lbl'Stop'Map{}())] + sort SortOps{} [] + sort SortAccountsCell{} [] + sort SortAccountCell{} [] + +// symbols + symbol Lbl'Hash'finish'Unds'SAME-NAME-DIFF-VALUE'Unds'NoOp{}() : SortNoOp{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(19,21,19,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}) : SortOp{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(17,19,17,34)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(SortInt{}, SortInt{}, SortInt{}) : SortOp{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(16,19,16,47)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + hooked-symbol Lbl'Stop'AccountCellMap{}() : SortAccountCellMap{} [function{}(), hook{}("MAP.unit")] + hooked-symbol Lbl'Stop'List{}() : SortList{} [function{}(), functional{}(), hook{}("LIST.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(937,19,937,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_nil"), symbol'Kywd'{}(".List"), total{}()] + hooked-symbol Lbl'Stop'Map{}() : SortMap{} [function{}(), functional{}(), hook{}("MAP.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(248,18,248,96)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Map"), total{}()] + hooked-symbol Lbl'Stop'Set{}() : SortSet{} [function{}(), functional{}(), hook{}("SET.unit"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(729,18,729,90)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}(".Set"), total{}()] + symbol Lbl'-LT-'account'-GT-'{}(SortAcctIDCell{}, SortBalanceCell{}) : SortAccountCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(8,21,11,31)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'-LT-'account'-GT-'-fragment{}(SortAcctIDCellOpt{}, SortBalanceCellOpt{}) : SortAccountCellFragment{} [constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'accounts'-GT-'{}(SortAccountCellMap{}) : SortAccountsCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(7,19,12,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'-LT-'accounts'-GT-'-fragment{}(SortAccountCellMap{}) : SortAccountsCellFragment{} [constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'acctID'-GT-'{}(SortInt{}) : SortAcctIDCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(9,25,9,72)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'-LT-'balance'-GT-'{}(SortInt{}) : SortBalanceCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(10,25,10,73)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'-LT-'generatedCounter'-GT-'{}(SortInt{}) : SortGeneratedCounterCell{} [cell{}(), constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'generatedTop'-GT-'{}(SortKCell{}, SortAccountsCell{}, SortGeneratedCounterCell{}) : SortGeneratedTopCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,19,12,30)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + symbol Lbl'-LT-'generatedTop'-GT-'-fragment{}(SortKCellOpt{}, SortAccountsCellOpt{}) : SortGeneratedTopCellFragment{} [constructor{}(), functional{}(), injective{}()] + symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [cell{}(), constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(6,19,6,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + hooked-symbol LblAccountCellMap'Coln'in'Unds'keys{}(SortAcctIDCell{}, SortAccountCellMap{}) : SortBool{} [function{}(), functional{}(), hook{}("MAP.in_keys"), total{}()] + hooked-symbol LblAccountCellMapItem{}(SortAcctIDCell{}, SortAccountCell{}) : SortAccountCellMap{} [function{}(), hook{}("MAP.element")] + symbol LblAccountCellMapKey{}(SortAccountCell{}) : SortAcctIDCell{} [function{}(), functional{}(), total{}()] + hooked-symbol LblList'Coln'get{}(SortList{}, SortInt{}) : SortKItem{} [function{}(), hook{}("LIST.get"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(965,20,965,91)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:get")] + hooked-symbol LblList'Coln'range{}(SortList{}, SortInt{}, SortInt{}) : SortList{} [function{}(), hook{}("LIST.range"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1012,19,1012,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:range")] + hooked-symbol LblList'Coln'set{}(SortList{}, SortInt{}, SortKItem{}) : SortList{} [function{}(), hook{}("LIST.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(974,19,974,108)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("List:set")] + hooked-symbol LblListItem{}(SortKItem{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.element"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(945,19,945,124)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_elem"), symbol'Kywd'{}("ListItem"), total{}()] + hooked-symbol LblMap'Coln'choice{}(SortMap{}) : SortKItem{} [function{}(), hook{}("MAP.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(393,20,393,101)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:choice")] + hooked-symbol LblMap'Coln'lookup{}(SortMap{}, SortKItem{}) : SortKItem{} [function{}(), hook{}("MAP.lookup"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(271,20,271,105)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookup")] + hooked-symbol LblMap'Coln'lookupOrDefault{}(SortMap{}, SortKItem{}, SortKItem{}) : SortKItem{} [function{}(), functional{}(), hook{}("MAP.lookupOrDefault"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(281,20,281,134)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:lookupOrDefault"), total{}()] + hooked-symbol LblMap'Coln'update{}(SortMap{}, SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.update"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(290,18,290,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Map:update"), total{}()] + hooked-symbol LblSet'Coln'choice{}(SortSet{}) : SortKItem{} [function{}(), hook{}("SET.choice"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(804,20,804,95)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:choice")] + hooked-symbol LblSet'Coln'difference{}(SortSet{}, SortSet{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.difference"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(769,18,769,106)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:difference"), total{}()] + hooked-symbol LblSet'Coln'in{}(SortKItem{}, SortSet{}) : SortBool{} [function{}(), functional{}(), hook{}("SET.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(777,19,777,94)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("Set:in"), total{}()] + hooked-symbol LblSetItem{}(SortKItem{}) : SortSet{} [function{}(), functional{}(), hook{}("SET.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(737,18,737,111)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("SetItem"), total{}()] + hooked-symbol Lbl'UndsPerc'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1248,18,1250,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (or (= 0 (mod #1 #2)) (>= #1 0)) (mod #1 #2) (ite (> #2 0) (- (mod #1 #2) #2) (+ (mod #1 #2) #2)))"), symbol'Kywd'{}("_%Int_")] + hooked-symbol Lbl'UndsAnd-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1261,18,1261,125)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("andInt"), symbol'Kywd'{}("_&Int_"), total{}()] + hooked-symbol Lbl'UndsStar'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.mul"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1242,18,1242,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("*"), symbol'Kywd'{}("_*Int_"), total{}()] + hooked-symbol Lbl'UndsPlus'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.add"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1255,18,1255,122)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("+"), symbol'Kywd'{}("_+Int_"), total{}()] + hooked-symbol Lbl'Unds'-Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.sub"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1256,18,1256,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("-"), symbol'Kywd'{}("_-Int_"), 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'UndsSlsh'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.tdiv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1245,18,1247,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (or (= 0 (mod #1 #2)) (>= #1 0)) (div #1 #2) (ite (> #2 0) (+ (div #1 #2) 1) (- (div #1 #2) 1)))"), symbol'Kywd'{}("_/Int_")] + hooked-symbol Lbl'Unds-LT--LT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shl"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1259,18,1259,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shlInt"), symbol'Kywd'{}("_<="), symbol'Kywd'{}("_>=Int_"), total{}()] + hooked-symbol Lbl'Unds-GT--GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.shr"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1258,18,1258,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("shrInt"), symbol'Kywd'{}("_>>Int_")] + hooked-symbol Lbl'Unds-GT-'Int'Unds'{}(SortInt{}, SortInt{}) : SortBool{} [function{}(), functional{}(), hook{}("INT.gt"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1320,19,1320,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}(">"), symbol'Kywd'{}("_>Int_"), total{}()] + hooked-symbol Lbl'Unds'AccountCellMap'Unds'{}(SortAccountCellMap{}, SortAccountCellMap{}) : SortAccountCellMap{} [element{}(LblAccountCellMapItem{}()), function{}(), hook{}("MAP.concat"), unit{}(Lbl'Stop'AccountCellMap{}())] + hooked-symbol Lbl'Unds'List'Unds'{}(SortList{}, SortList{}) : SortList{} [element{}(LblListItem{}()), function{}(), functional{}(), hook{}("LIST.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(929,19,929,198)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_concat"), symbol'Kywd'{}("_List_"), total{}(), unit{}(Lbl'Stop'List{}()), update{}(LblList'Coln'set{}())] + hooked-symbol Lbl'Unds'Map'Unds'{}(SortMap{}, SortMap{}) : SortMap{} [element{}(Lbl'UndsPipe'-'-GT-Unds'{}()), function{}(), hook{}("MAP.concat"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(240,18,240,165)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Map_"), unit{}(Lbl'Stop'Map{}())] + hooked-symbol Lbl'Unds'Set'Unds'{}(SortSet{}, SortSet{}) : SortSet{} [element{}(LblSetItem{}()), function{}(), hook{}("SET.concat"), idem{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(721,18,721,157)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_Set_"), unit{}(Lbl'Stop'Set{}())] + hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(SortMap{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.remove"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(299,18,299,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_[_<-undef]"), total{}()] + hooked-symbol Lbl'UndsXor-Perc'Int'UndsUnds'{}(SortInt{}, SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.powmod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1240,18,1240,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(mod (^ #1 #2) #3)"), symbol'Kywd'{}("_^%Int__")] + hooked-symbol Lbl'UndsXor-'Int'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.pow"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1239,18,1239,109)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("^"), symbol'Kywd'{}("_^Int_")] + hooked-symbol Lbl'Unds'andBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.and"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1110,19,1110,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andBool_"), total{}()] + hooked-symbol Lbl'Unds'andThenBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.andThen"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1111,19,1111,146)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("and"), symbol'Kywd'{}("_andThenBool_"), total{}()] + hooked-symbol Lbl'Unds'divInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.ediv"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1252,18,1252,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("div"), symbol'Kywd'{}("_divInt_")] + 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(1331,19,1331,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Unds'impliesBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.implies"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1115,19,1115,145)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("=>"), symbol'Kywd'{}("_impliesBool_"), total{}()] + hooked-symbol Lbl'Unds'inList'Unds'{}(SortKItem{}, SortList{}) : SortBool{} [function{}(), functional{}(), hook{}("LIST.in"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1021,19,1021,97)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("_inList_"), 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol Lbl'Unds'modInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), hook{}("INT.emod"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1253,18,1253,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("mod"), symbol'Kywd'{}("_modInt_")] + hooked-symbol Lbl'Unds'orBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.or"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1113,19,1113,135)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orBool_"), total{}()] + hooked-symbol Lbl'Unds'orElseBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.orElse"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1114,19,1114,143)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("or"), symbol'Kywd'{}("_orElseBool_"), total{}()] + hooked-symbol Lbl'Unds'xorBool'Unds'{}(SortBool{}, SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1112,19,1112,138)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("xor"), symbol'Kywd'{}("_xorBool_"), total{}()] + hooked-symbol Lbl'Unds'xorInt'Unds'{}(SortInt{}, SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.xor"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1263,18,1263,127)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("xorInt"), symbol'Kywd'{}("_xorInt_"), total{}()] + hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(SortKItem{}, SortKItem{}) : SortMap{} [function{}(), functional{}(), hook{}("MAP.element"), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(257,18,257,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1265,18,1265,123)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("orInt"), symbol'Kywd'{}("_|Int_"), 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/robertorosmaninho/rv/k/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(1282,18,1282,119)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 0) (- 0 #1) #1)"), total{}()] + 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(1307,18,1307,103)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + symbol LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [freshGenerator{}(), function{}(), functional{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1445,18,1445,77)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol LblgetGeneratedCounterCell{}(SortGeneratedTopCell{}) : SortGeneratedCounterCell{} [function{}()] + symbol LblinitAccountCell{}() : SortAccountCellMap{} [function{}(), functional{}(), total{}()] + symbol LblinitAccountsCell{}() : SortAccountsCell{} [function{}(), functional{}(), total{}()] + symbol LblinitAcctIDCell{}() : SortAcctIDCell{} [function{}(), functional{}(), total{}()] + symbol LblinitBalanceCell{}() : SortBalanceCell{} [function{}(), functional{}(), total{}()] + symbol LblinitGeneratedCounterCell{}() : SortGeneratedCounterCell{} [function{}(), functional{}(), total{}()] + symbol LblinitGeneratedTopCell{}(SortMap{}) : SortGeneratedTopCell{} [function{}()] + symbol LblinitKCell{}(SortMap{}) : SortKCell{} [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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol LblisAccountCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAccountCellFragment{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAccountCellMap{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAccountsCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAccountsCellFragment{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAccountsCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAcctIDCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisAcctIDCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisBalanceCell{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisBalanceCellOpt{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisBool{}(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 LblisMap{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisNoOp{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisOp{}(SortK{}) : SortBool{} [function{}(), functional{}(), total{}()] + symbol LblisOps{}(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(2297,26,2297,132)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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(1293,18,1293,75)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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(1274,18,1274,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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(1273,18,1273,114)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("(ite (< #1 #2) #1 #2)"), total{}()] + symbol LblnoAccountsCell{}() : SortAccountsCellOpt{} [constructor{}(), functional{}(), injective{}()] + symbol LblnoAcctIDCell{}() : SortAcctIDCellOpt{} [constructor{}(), functional{}(), injective{}()] + symbol LblnoBalanceCell{}() : SortBalanceCellOpt{} [constructor{}(), functional{}(), injective{}()] + symbol LblnoKCell{}() : SortKCellOpt{} [constructor{}(), functional{}(), injective{}()] + hooked-symbol LblnotBool'Unds'{}(SortBool{}) : SortBool{} [function{}(), functional{}(), hook{}("BOOL.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1109,19,1109,131)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smt-hook{}("not"), symbol'Kywd'{}("notBool_"), total{}()] + symbol Lblproject'Coln'AccountCell{}(SortK{}) : SortAccountCell{} [function{}()] + symbol Lblproject'Coln'AccountCellFragment{}(SortK{}) : SortAccountCellFragment{} [function{}()] + symbol Lblproject'Coln'AccountCellMap{}(SortK{}) : SortAccountCellMap{} [function{}()] + symbol Lblproject'Coln'AccountsCell{}(SortK{}) : SortAccountsCell{} [function{}()] + symbol Lblproject'Coln'AccountsCellFragment{}(SortK{}) : SortAccountsCellFragment{} [function{}()] + symbol Lblproject'Coln'AccountsCellOpt{}(SortK{}) : SortAccountsCellOpt{} [function{}()] + symbol Lblproject'Coln'AcctIDCell{}(SortK{}) : SortAcctIDCell{} [function{}()] + symbol Lblproject'Coln'AcctIDCellOpt{}(SortK{}) : SortAcctIDCellOpt{} [function{}()] + symbol Lblproject'Coln'BalanceCell{}(SortK{}) : SortBalanceCell{} [function{}()] + symbol Lblproject'Coln'BalanceCellOpt{}(SortK{}) : SortBalanceCellOpt{} [function{}()] + symbol Lblproject'Coln'Bool{}(SortK{}) : SortBool{} [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'Map{}(SortK{}) : SortMap{} [function{}()] + symbol Lblproject'Coln'NoOp{}(SortK{}) : SortNoOp{} [function{}()] + symbol Lblproject'Coln'Op{}(SortK{}) : SortOp{} [function{}()] + symbol Lblproject'Coln'Ops{}(SortK{}) : SortOps{} [function{}()] + symbol Lblproject'Coln'Set{}(SortK{}) : SortSet{} [function{}()] + hooked-symbol LblpushList{}(SortKItem{}, SortList{}) : SortList{} [function{}(), functional{}(), hook{}("LIST.push"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(953,19,953,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("pushList"), total{}()] + hooked-symbol LblrandInt'LParUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int{}(SortInt{}) : SortInt{} [function{}(), hook{}("INT.rand"), impure{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1341,18,1341,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + symbol Lblseq{}(SortOp{}, SortOps{}) : SortOps{} [constructor{}(), functional{}(), injective{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(14,20,14,44)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)"), symbol'Kywd'{}("seq")] + 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(1308,18,1308,113)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), total{}()] + hooked-symbol LblsizeList{}(SortList{}) : SortInt{} [function{}(), functional{}(), hook{}("LIST.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1029,18,1029,116)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("smt_seq_len"), symbol'Kywd'{}("sizeList"), total{}()] + hooked-symbol LblsizeMap{}(SortMap{}) : SortInt{} [function{}(), functional{}(), hook{}("MAP.size"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(373,18,373,99)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), symbol'Kywd'{}("sizeMap"), total{}()] + hooked-symbol LblsrandInt'LParUndsRParUnds'INT-COMMON'Unds'K'Unds'Int{}(SortInt{}) : SortK{} [function{}(), hook{}("INT.srand"), impure{}(), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1342,16,1342,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + hooked-symbol Lbl'Tild'Int'Unds'{}(SortInt{}) : SortInt{} [function{}(), functional{}(), hook{}("INT.not"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(1237,18,1237,112)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)"), smtlib{}("notInt"), symbol'Kywd'{}("~Int_"), total{}()] + +// generated axioms + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountsCellOpt{}, SortKItem{}} (From:SortAccountsCellOpt{}))) [subsort{SortAccountsCellOpt{}, SortKItem{}}()] // subsort + 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: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{SortMap{}, SortKItem{}} (From:SortMap{}))) [subsort{SortMap{}, SortKItem{}}()] // 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:SortAcctIDCellOpt{}, \equals{SortAcctIDCellOpt{}, R} (Val:SortAcctIDCellOpt{}, inj{SortAcctIDCell{}, SortAcctIDCellOpt{}} (From:SortAcctIDCell{}))) [subsort{SortAcctIDCell{}, SortAcctIDCellOpt{}}()] // 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{SortBalanceCell{}, SortKItem{}} (From:SortBalanceCell{}))) [subsort{SortBalanceCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortAccountsCellOpt{}, \equals{SortAccountsCellOpt{}, R} (Val:SortAccountsCellOpt{}, inj{SortAccountsCell{}, SortAccountsCellOpt{}} (From:SortAccountsCell{}))) [subsort{SortAccountsCell{}, SortAccountsCellOpt{}}()] // 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{SortGeneratedTopCell{}, SortKItem{}} (From:SortGeneratedTopCell{}))) [subsort{SortGeneratedTopCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortOps{}, SortKItem{}} (From:SortOps{}))) [subsort{SortOps{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountCellMap{}, SortKItem{}} (From:SortAccountCellMap{}))) [subsort{SortAccountCellMap{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountsCell{}, SortKItem{}} (From:SortAccountsCell{}))) [subsort{SortAccountsCell{}, 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{SortBool{}, SortKItem{}} (From:SortBool{}))) [subsort{SortBool{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortBalanceCellOpt{}, \equals{SortBalanceCellOpt{}, R} (Val:SortBalanceCellOpt{}, inj{SortBalanceCell{}, SortBalanceCellOpt{}} (From:SortBalanceCell{}))) [subsort{SortBalanceCell{}, SortBalanceCellOpt{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountsCellFragment{}, SortKItem{}} (From:SortAccountsCellFragment{}))) [subsort{SortAccountsCellFragment{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortOp{}, SortKItem{}} (From:SortOp{}))) [subsort{SortOp{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAcctIDCell{}, SortKItem{}} (From:SortAcctIDCell{}))) [subsort{SortAcctIDCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountCellFragment{}, SortKItem{}} (From:SortAccountCellFragment{}))) [subsort{SortAccountCellFragment{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortAccountCellMap{}, \equals{SortAccountCellMap{}, R} (Val:SortAccountCellMap{}, inj{SortAccountCell{}, SortAccountCellMap{}} (From:SortAccountCell{}))) [subsort{SortAccountCell{}, SortAccountCellMap{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortBalanceCellOpt{}, SortKItem{}} (From:SortBalanceCellOpt{}))) [subsort{SortBalanceCellOpt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortNoOp{}, SortKItem{}} (From:SortNoOp{}))) [subsort{SortNoOp{}, 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{SortInt{}, SortKItem{}} (From:SortInt{}))) [subsort{SortInt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAcctIDCellOpt{}, SortKItem{}} (From:SortAcctIDCellOpt{}))) [subsort{SortAcctIDCellOpt{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, inj{SortAccountCell{}, SortKItem{}} (From:SortAccountCell{}))) [subsort{SortAccountCell{}, SortKItem{}}()] // subsort + axiom{R} \exists{R} (Val:SortOps{}, \equals{SortOps{}, R} (Val:SortOps{}, inj{SortOp{}, SortOps{}} (From:SortOp{}))) [subsort{SortOp{}, SortOps{}}()] // 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:SortNoOp{}, \equals{SortNoOp{}, R} (Val:SortNoOp{}, Lbl'Hash'finish'Unds'SAME-NAME-DIFF-VALUE'Unds'NoOp{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortOp{}, \equals{SortOp{}, R} (Val:SortOp{}, Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(K0:SortInt{}, K1:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortOp{}} (\and{SortOp{}} (Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(X0:SortInt{}, X1:SortInt{}), Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(Y0:SortInt{}, Y1:SortInt{})), Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}), \and{SortInt{}} (X1:SortInt{}, Y1:SortInt{}))) [constructor{}()] // no confusion same constructor + axiom{}\not{SortOp{}} (\and{SortOp{}} (Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(X0:SortInt{}, X1:SortInt{}), Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(Y0:SortInt{}, Y1:SortInt{}, Y2:SortInt{}))) [constructor{}()] // no confusion different constructors + axiom{R} \exists{R} (Val:SortOp{}, \equals{SortOp{}, R} (Val:SortOp{}, Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(K0:SortInt{}, K1:SortInt{}, K2:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortOp{}} (\and{SortOp{}} (Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(X0:SortInt{}, X1:SortInt{}, X2:SortInt{}), Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(Y0:SortInt{}, Y1:SortInt{}, Y2:SortInt{})), Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}), \and{SortInt{}} (X1:SortInt{}, Y1:SortInt{}), \and{SortInt{}} (X2:SortInt{}, Y2:SortInt{}))) [constructor{}()] // no confusion same constructor + 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:SortAccountCell{}, \equals{SortAccountCell{}, R} (Val:SortAccountCell{}, Lbl'-LT-'account'-GT-'{}(K0:SortAcctIDCell{}, K1:SortBalanceCell{}))) [functional{}()] // functional + axiom{}\implies{SortAccountCell{}} (\and{SortAccountCell{}} (Lbl'-LT-'account'-GT-'{}(X0:SortAcctIDCell{}, X1:SortBalanceCell{}), Lbl'-LT-'account'-GT-'{}(Y0:SortAcctIDCell{}, Y1:SortBalanceCell{})), Lbl'-LT-'account'-GT-'{}(\and{SortAcctIDCell{}} (X0:SortAcctIDCell{}, Y0:SortAcctIDCell{}), \and{SortBalanceCell{}} (X1:SortBalanceCell{}, Y1:SortBalanceCell{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortAccountCellFragment{}, \equals{SortAccountCellFragment{}, R} (Val:SortAccountCellFragment{}, Lbl'-LT-'account'-GT-'-fragment{}(K0:SortAcctIDCellOpt{}, K1:SortBalanceCellOpt{}))) [functional{}()] // functional + axiom{}\implies{SortAccountCellFragment{}} (\and{SortAccountCellFragment{}} (Lbl'-LT-'account'-GT-'-fragment{}(X0:SortAcctIDCellOpt{}, X1:SortBalanceCellOpt{}), Lbl'-LT-'account'-GT-'-fragment{}(Y0:SortAcctIDCellOpt{}, Y1:SortBalanceCellOpt{})), Lbl'-LT-'account'-GT-'-fragment{}(\and{SortAcctIDCellOpt{}} (X0:SortAcctIDCellOpt{}, Y0:SortAcctIDCellOpt{}), \and{SortBalanceCellOpt{}} (X1:SortBalanceCellOpt{}, Y1:SortBalanceCellOpt{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortAccountsCell{}, \equals{SortAccountsCell{}, R} (Val:SortAccountsCell{}, Lbl'-LT-'accounts'-GT-'{}(K0:SortAccountCellMap{}))) [functional{}()] // functional + axiom{}\implies{SortAccountsCell{}} (\and{SortAccountsCell{}} (Lbl'-LT-'accounts'-GT-'{}(X0:SortAccountCellMap{}), Lbl'-LT-'accounts'-GT-'{}(Y0:SortAccountCellMap{})), Lbl'-LT-'accounts'-GT-'{}(\and{SortAccountCellMap{}} (X0:SortAccountCellMap{}, Y0:SortAccountCellMap{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortAccountsCellFragment{}, \equals{SortAccountsCellFragment{}, R} (Val:SortAccountsCellFragment{}, Lbl'-LT-'accounts'-GT-'-fragment{}(K0:SortAccountCellMap{}))) [functional{}()] // functional + axiom{}\implies{SortAccountsCellFragment{}} (\and{SortAccountsCellFragment{}} (Lbl'-LT-'accounts'-GT-'-fragment{}(X0:SortAccountCellMap{}), Lbl'-LT-'accounts'-GT-'-fragment{}(Y0:SortAccountCellMap{})), Lbl'-LT-'accounts'-GT-'-fragment{}(\and{SortAccountCellMap{}} (X0:SortAccountCellMap{}, Y0:SortAccountCellMap{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortAcctIDCell{}, \equals{SortAcctIDCell{}, R} (Val:SortAcctIDCell{}, Lbl'-LT-'acctID'-GT-'{}(K0:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortAcctIDCell{}} (\and{SortAcctIDCell{}} (Lbl'-LT-'acctID'-GT-'{}(X0:SortInt{}), Lbl'-LT-'acctID'-GT-'{}(Y0:SortInt{})), Lbl'-LT-'acctID'-GT-'{}(\and{SortInt{}} (X0:SortInt{}, Y0:SortInt{}))) [constructor{}()] // no confusion same constructor + axiom{R} \exists{R} (Val:SortBalanceCell{}, \equals{SortBalanceCell{}, R} (Val:SortBalanceCell{}, Lbl'-LT-'balance'-GT-'{}(K0:SortInt{}))) [functional{}()] // functional + axiom{}\implies{SortBalanceCell{}} (\and{SortBalanceCell{}} (Lbl'-LT-'balance'-GT-'{}(X0:SortInt{}), Lbl'-LT-'balance'-GT-'{}(Y0:SortInt{})), Lbl'-LT-'balance'-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:SortAccountsCell{}, K2:SortGeneratedCounterCell{}))) [functional{}()] // functional + axiom{}\implies{SortGeneratedTopCell{}} (\and{SortGeneratedTopCell{}} (Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortAccountsCell{}, X2:SortGeneratedCounterCell{}), Lbl'-LT-'generatedTop'-GT-'{}(Y0:SortKCell{}, Y1:SortAccountsCell{}, Y2:SortGeneratedCounterCell{})), Lbl'-LT-'generatedTop'-GT-'{}(\and{SortKCell{}} (X0:SortKCell{}, Y0:SortKCell{}), \and{SortAccountsCell{}} (X1:SortAccountsCell{}, Y1:SortAccountsCell{}), \and{SortGeneratedCounterCell{}} (X2:SortGeneratedCounterCell{}, Y2: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:SortAccountsCellOpt{}))) [functional{}()] // functional + axiom{}\implies{SortGeneratedTopCellFragment{}} (\and{SortGeneratedTopCellFragment{}} (Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortAccountsCellOpt{}), Lbl'-LT-'generatedTop'-GT-'-fragment{}(Y0:SortKCellOpt{}, Y1:SortAccountsCellOpt{})), Lbl'-LT-'generatedTop'-GT-'-fragment{}(\and{SortKCellOpt{}} (X0:SortKCellOpt{}, Y0:SortKCellOpt{}), \and{SortAccountsCellOpt{}} (X1:SortAccountsCellOpt{}, Y1:SortAccountsCellOpt{}))) [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:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblAccountCellMap'Coln'in'Unds'keys{}(K0:SortAcctIDCell{}, K1:SortAccountCellMap{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortAcctIDCell{}, \equals{SortAcctIDCell{}, R} (Val:SortAcctIDCell{}, LblAccountCellMapKey{}(K0:SortAccountCell{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortList{}, \equals{SortList{}, R} (Val:SortList{}, LblListItem{}(K0:SortKItem{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortKItem{}, \equals{SortKItem{}, R} (Val:SortKItem{}, LblMap'Coln'lookupOrDefault{}(K0:SortMap{}, K1:SortKItem{}, K2: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{SortAccountCellMap{}, R} (Lbl'Unds'AccountCellMap'Unds'{}(Lbl'Unds'AccountCellMap'Unds'{}(K1:SortAccountCellMap{},K2:SortAccountCellMap{}),K3:SortAccountCellMap{}),Lbl'Unds'AccountCellMap'Unds'{}(K1:SortAccountCellMap{},Lbl'Unds'AccountCellMap'Unds'{}(K2:SortAccountCellMap{},K3:SortAccountCellMap{}))) [assoc{}()] // associativity + axiom{R}\equals{SortAccountCellMap{}, R} (Lbl'Unds'AccountCellMap'Unds'{}(K:SortAccountCellMap{},Lbl'Stop'AccountCellMap{}()),K:SortAccountCellMap{}) [unit{}()] // right unit + axiom{R}\equals{SortAccountCellMap{}, R} (Lbl'Unds'AccountCellMap'Unds'{}(Lbl'Stop'AccountCellMap{}(),K:SortAccountCellMap{}),K:SortAccountCellMap{}) [unit{}()] // left unit + 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: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'inList'Unds'{}(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:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblfreshInt'LParUndsRParUnds'INT'Unds'Int'Unds'Int{}(K0:SortInt{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortAccountCellMap{}, \equals{SortAccountCellMap{}, R} (Val:SortAccountCellMap{}, LblinitAccountCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortAccountsCell{}, \equals{SortAccountsCell{}, R} (Val:SortAccountsCell{}, LblinitAccountsCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortAcctIDCell{}, \equals{SortAcctIDCell{}, R} (Val:SortAcctIDCell{}, LblinitAcctIDCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBalanceCell{}, \equals{SortBalanceCell{}, R} (Val:SortBalanceCell{}, LblinitBalanceCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortGeneratedCounterCell{}, \equals{SortGeneratedCounterCell{}, R} (Val:SortGeneratedCounterCell{}, LblinitGeneratedCounterCell{}())) [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{}, LblisAccountCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAccountCellFragment{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAccountCellMap{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAccountsCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAccountsCellFragment{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAccountsCellOpt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAcctIDCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisAcctIDCellOpt{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisBalanceCell{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisBalanceCellOpt{}(K0:SortK{}))) [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{}, 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{}, LblisMap{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisNoOp{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisOp{}(K0:SortK{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBool{}, \equals{SortBool{}, R} (Val:SortBool{}, LblisOps{}(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:SortAccountsCellOpt{}, \equals{SortAccountsCellOpt{}, R} (Val:SortAccountsCellOpt{}, LblnoAccountsCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortAcctIDCellOpt{}, \equals{SortAcctIDCellOpt{}, R} (Val:SortAcctIDCellOpt{}, LblnoAcctIDCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortBalanceCellOpt{}, \equals{SortBalanceCellOpt{}, R} (Val:SortBalanceCellOpt{}, LblnoBalanceCell{}())) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortKCellOpt{}, \equals{SortKCellOpt{}, R} (Val:SortKCellOpt{}, LblnoKCell{}())) [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:SortOps{}, \equals{SortOps{}, R} (Val:SortOps{}, Lblseq{}(K0:SortOp{}, K1:SortOps{}))) [functional{}()] // functional + axiom{}\implies{SortOps{}} (\and{SortOps{}} (Lblseq{}(X0:SortOp{}, X1:SortOps{}), Lblseq{}(Y0:SortOp{}, Y1:SortOps{})), Lblseq{}(\and{SortOp{}} (X0:SortOp{}, Y0:SortOp{}), \and{SortOps{}} (X1:SortOps{}, Y1:SortOps{}))) [constructor{}()] // no confusion same constructor + 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:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblsizeList{}(K0:SortList{}))) [functional{}()] // functional + axiom{R} \exists{R} (Val:SortInt{}, \equals{SortInt{}, R} (Val:SortInt{}, LblsizeMap{}(K0:SortMap{}))) [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{SortAccountCell{}} (\exists{SortAccountCell{}} (X0:SortAcctIDCell{}, \exists{SortAccountCell{}} (X1:SortBalanceCell{}, Lbl'-LT-'account'-GT-'{}(X0:SortAcctIDCell{}, X1:SortBalanceCell{}))), \bottom{SortAccountCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortAccountCellFragment{}} (\exists{SortAccountCellFragment{}} (X0:SortAcctIDCellOpt{}, \exists{SortAccountCellFragment{}} (X1:SortBalanceCellOpt{}, Lbl'-LT-'account'-GT-'-fragment{}(X0:SortAcctIDCellOpt{}, X1:SortBalanceCellOpt{}))), \bottom{SortAccountCellFragment{}}()) [constructor{}()] // no junk + axiom{} \or{SortAccountCellMap{}} (\exists{SortAccountCellMap{}} (Val:SortAccountCell{}, inj{SortAccountCell{}, SortAccountCellMap{}} (Val:SortAccountCell{})), \bottom{SortAccountCellMap{}}()) [constructor{}()] // no junk + axiom{} \or{SortAccountsCell{}} (\exists{SortAccountsCell{}} (X0:SortAccountCellMap{}, Lbl'-LT-'accounts'-GT-'{}(X0:SortAccountCellMap{})), \bottom{SortAccountsCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortAccountsCellFragment{}} (\exists{SortAccountsCellFragment{}} (X0:SortAccountCellMap{}, Lbl'-LT-'accounts'-GT-'-fragment{}(X0:SortAccountCellMap{})), \bottom{SortAccountsCellFragment{}}()) [constructor{}()] // no junk + axiom{} \or{SortAccountsCellOpt{}} (LblnoAccountsCell{}(), \exists{SortAccountsCellOpt{}} (Val:SortAccountsCell{}, inj{SortAccountsCell{}, SortAccountsCellOpt{}} (Val:SortAccountsCell{})), \bottom{SortAccountsCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortAcctIDCell{}} (\exists{SortAcctIDCell{}} (X0:SortInt{}, Lbl'-LT-'acctID'-GT-'{}(X0:SortInt{})), \bottom{SortAcctIDCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortAcctIDCellOpt{}} (LblnoAcctIDCell{}(), \exists{SortAcctIDCellOpt{}} (Val:SortAcctIDCell{}, inj{SortAcctIDCell{}, SortAcctIDCellOpt{}} (Val:SortAcctIDCell{})), \bottom{SortAcctIDCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortBalanceCell{}} (\exists{SortBalanceCell{}} (X0:SortInt{}, Lbl'-LT-'balance'-GT-'{}(X0:SortInt{})), \bottom{SortBalanceCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortBalanceCellOpt{}} (LblnoBalanceCell{}(), \exists{SortBalanceCellOpt{}} (Val:SortBalanceCell{}, inj{SortBalanceCell{}, SortBalanceCellOpt{}} (Val:SortBalanceCell{})), \bottom{SortBalanceCellOpt{}}()) [constructor{}()] // no junk + axiom{} \or{SortBool{}} (\top{SortBool{}}(), \bottom{SortBool{}}()) [constructor{}()] // no junk (TODO: fix bug with \dv) + 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:SortAccountsCell{}, \exists{SortGeneratedTopCell{}} (X2:SortGeneratedCounterCell{}, Lbl'-LT-'generatedTop'-GT-'{}(X0:SortKCell{}, X1:SortAccountsCell{}, X2:SortGeneratedCounterCell{})))), \bottom{SortGeneratedTopCell{}}()) [constructor{}()] // no junk + axiom{} \or{SortGeneratedTopCellFragment{}} (\exists{SortGeneratedTopCellFragment{}} (X0:SortKCellOpt{}, \exists{SortGeneratedTopCellFragment{}} (X1:SortAccountsCellOpt{}, Lbl'-LT-'generatedTop'-GT-'-fragment{}(X0:SortKCellOpt{}, X1:SortAccountsCellOpt{}))), \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{}} (Val:SortAccountCell{}, inj{SortAccountCell{}, SortKItem{}} (Val:SortAccountCell{})), \exists{SortKItem{}} (Val:SortAccountCellFragment{}, inj{SortAccountCellFragment{}, SortKItem{}} (Val:SortAccountCellFragment{})), \exists{SortKItem{}} (Val:SortAccountCellMap{}, inj{SortAccountCellMap{}, SortKItem{}} (Val:SortAccountCellMap{})), \exists{SortKItem{}} (Val:SortAccountsCell{}, inj{SortAccountsCell{}, SortKItem{}} (Val:SortAccountsCell{})), \exists{SortKItem{}} (Val:SortAccountsCellFragment{}, inj{SortAccountsCellFragment{}, SortKItem{}} (Val:SortAccountsCellFragment{})), \exists{SortKItem{}} (Val:SortAccountsCellOpt{}, inj{SortAccountsCellOpt{}, SortKItem{}} (Val:SortAccountsCellOpt{})), \exists{SortKItem{}} (Val:SortAcctIDCell{}, inj{SortAcctIDCell{}, SortKItem{}} (Val:SortAcctIDCell{})), \exists{SortKItem{}} (Val:SortAcctIDCellOpt{}, inj{SortAcctIDCellOpt{}, SortKItem{}} (Val:SortAcctIDCellOpt{})), \exists{SortKItem{}} (Val:SortBalanceCell{}, inj{SortBalanceCell{}, SortKItem{}} (Val:SortBalanceCell{})), \exists{SortKItem{}} (Val:SortBalanceCellOpt{}, inj{SortBalanceCellOpt{}, SortKItem{}} (Val:SortBalanceCellOpt{})), \exists{SortKItem{}} (Val:SortBool{}, inj{SortBool{}, SortKItem{}} (Val:SortBool{})), \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:SortMap{}, inj{SortMap{}, SortKItem{}} (Val:SortMap{})), \exists{SortKItem{}} (Val:SortNoOp{}, inj{SortNoOp{}, SortKItem{}} (Val:SortNoOp{})), \exists{SortKItem{}} (Val:SortOp{}, inj{SortOp{}, SortKItem{}} (Val:SortOp{})), \exists{SortKItem{}} (Val:SortOps{}, inj{SortOps{}, SortKItem{}} (Val:SortOps{})), \exists{SortKItem{}} (Val:SortSet{}, inj{SortSet{}, SortKItem{}} (Val:SortSet{})), \bottom{SortKItem{}}()) [constructor{}()] // no junk + axiom{} \or{SortNoOp{}} (Lbl'Hash'finish'Unds'SAME-NAME-DIFF-VALUE'Unds'NoOp{}(), \bottom{SortNoOp{}}()) [constructor{}()] // no junk + axiom{} \or{SortOp{}} (\exists{SortOp{}} (X0:SortInt{}, \exists{SortOp{}} (X1:SortInt{}, Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(X0:SortInt{}, X1:SortInt{}))), \exists{SortOp{}} (X0:SortInt{}, \exists{SortOp{}} (X1:SortInt{}, \exists{SortOp{}} (X2:SortInt{}, Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(X0:SortInt{}, X1:SortInt{}, X2:SortInt{})))), \bottom{SortOp{}}()) [constructor{}()] // no junk + axiom{} \or{SortOps{}} (\exists{SortOps{}} (X0:SortOp{}, \exists{SortOps{}} (X1:SortOps{}, Lblseq{}(X0:SortOp{}, X1:SortOps{}))), \exists{SortOps{}} (Val:SortOp{}, inj{SortOp{}, SortOps{}} (Val:SortOp{})), \bottom{SortOps{}}()) [constructor{}()] // no junk + +// rules +// rule ``(``(inj{Op,KItem}(`#transferFunds____SAME-NAME-DIFF-VALUE_Op_Int_Int_Int`(ACCT,ACCT,VALUE))~>_DotVar1),``(`_AccountCellMap_`(`AccountCellMapItem`(``(ACCT),``(``(ACCT),``(ORIGFROM))),_DotVar2)) #as _Gen4,_DotVar0)=>``(``(_DotVar1),_Gen4,_DotVar0) requires `_<=Int_`(VALUE,ORIGFROM) ensures #token("true","Bool") [UNIQUE_ID(a5128f0cdab350d79eb522296511efd216239a5334777350e8b2633b8d2df8dd), org.kframework.attributes.Location(Location(33,11,38,36)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOp{}, SortKItem{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(VarACCT:SortInt{},VarACCT:SortInt{},VarVALUE:SortInt{})),Var'Unds'DotVar1:SortK{})),\and{SortAccountsCell{}}(Lbl'-LT-'accounts'-GT-'{}(Lbl'Unds'AccountCellMap'Unds'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCT:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCT:SortInt{}),Lbl'-LT-'balance'-GT-'{}(VarORIGFROM:SortInt{}))),Var'Unds'DotVar2:SortAccountCellMap{})),Var'Unds'Gen4:SortAccountsCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \equals{SortBool{},SortGeneratedTopCell{}}( + Lbl'Unds-LT-Eqls'Int'Unds'{}(VarVALUE:SortInt{},VarORIGFROM:SortInt{}), + \dv{SortBool{}}("true"))), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(Var'Unds'DotVar1:SortK{}),Var'Unds'Gen4:SortAccountsCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("a5128f0cdab350d79eb522296511efd216239a5334777350e8b2633b8d2df8dd"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(33,11,38,36)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + +// rule ``(``(inj{Op,KItem}(`#transferFunds____SAME-NAME-DIFF-VALUE_Op_Int_Int_Int`(ACCTFROM,ACCTTO,VALUE))~>_DotVar1),``(`_AccountCellMap_`(`_AccountCellMap_`(`AccountCellMapItem`(``(ACCTFROM),``(``(ACCTFROM),``(ORIGFROM))),`AccountCellMapItem`(``(ACCTTO),``(``(ACCTTO),``(ORIGTO)))),_DotVar2)),_DotVar0)=>``(``(_DotVar1),``(`_AccountCellMap_`(`_AccountCellMap_`(`AccountCellMapItem`(``(ACCTFROM),``(``(ACCTFROM),``(`_-Int_`(ORIGFROM,VALUE)))),`AccountCellMapItem`(``(ACCTTO),``(``(ACCTTO),``(`_+Int_`(ORIGTO,VALUE))))),_DotVar2)),_DotVar0) requires `_andBool_`(`_=/=K_`(inj{Int,KItem}(ACCTFROM),inj{Int,KItem}(ACCTTO)),`_<=Int_`(VALUE,ORIGFROM)) ensures #token("true","Bool") [UNIQUE_ID(fb117284830b1006ce41cfae940f0b297d8ffe0aebdb4b041bb9fa6dcf1191dd), org.kframework.attributes.Location(Location(41,12,52,65)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)]), preserves-definedness] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOp{}, SortKItem{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(VarACCTFROM:SortInt{},VarACCTTO:SortInt{},VarVALUE:SortInt{})),Var'Unds'DotVar1:SortK{})),Lbl'-LT-'accounts'-GT-'{}(Lbl'Unds'AccountCellMap'Unds'{}(Lbl'Unds'AccountCellMap'Unds'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'balance'-GT-'{}(VarORIGFROM:SortInt{}))),LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTTO:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTTO:SortInt{}),Lbl'-LT-'balance'-GT-'{}(VarORIGTO:SortInt{})))),Var'Unds'DotVar2:SortAccountCellMap{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \equals{SortBool{},SortGeneratedTopCell{}}( + Lbl'Unds'andBool'Unds'{}(Lbl'UndsEqlsSlshEqls'K'Unds'{}(kseq{}(inj{SortInt{}, SortKItem{}}(VarACCTFROM:SortInt{}),dotk{}()),kseq{}(inj{SortInt{}, SortKItem{}}(VarACCTTO:SortInt{}),dotk{}())),Lbl'Unds-LT-Eqls'Int'Unds'{}(VarVALUE:SortInt{},VarORIGFROM:SortInt{})), + \dv{SortBool{}}("true"))), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(Var'Unds'DotVar1:SortK{}),Lbl'-LT-'accounts'-GT-'{}(Lbl'Unds'AccountCellMap'Unds'{}(Lbl'Unds'AccountCellMap'Unds'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'balance'-GT-'{}(Lbl'Unds'-Int'Unds'{}(VarORIGFROM:SortInt{},VarVALUE:SortInt{})))),LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTTO:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTTO:SortInt{}),Lbl'-LT-'balance'-GT-'{}(Lbl'UndsPlus'Int'Unds'{}(VarORIGTO:SortInt{},VarVALUE:SortInt{}))))),Var'Unds'DotVar2:SortAccountCellMap{})),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("fb117284830b1006ce41cfae940f0b297d8ffe0aebdb4b041bb9fa6dcf1191dd"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(41,12,52,65)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)"), preserves-definedness{}()] + +// rule ``(``(inj{Op,KItem}(`#transferFunds____SAME-NAME-DIFF-VALUE_Op_Int_Int_Int`(ACCTFROM,_ACCTTO,VALUE))~>_DotVar1),``(`_AccountCellMap_`(`AccountCellMapItem`(``(ACCTFROM),``(``(ACCTFROM),``(ORIGFROM))),_DotVar2)) #as _Gen4,_DotVar0)=>``(``(_DotVar1),_Gen4,_DotVar0) requires `_>Int_`(VALUE,ORIGFROM) ensures #token("true","Bool") [UNIQUE_ID(7ecf8b0075d5324c3b741216a581b50c347b4a0fd1587f8ffa2a6815e5b190f4), org.kframework.attributes.Location(Location(55,10,61,35)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOp{}, SortKItem{}}(Lbl'Hash'transferFunds'UndsUndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int'Unds'Int{}(VarACCTFROM:SortInt{},Var'Unds'ACCTTO:SortInt{},VarVALUE:SortInt{})),Var'Unds'DotVar1:SortK{})),\and{SortAccountsCell{}}(Lbl'-LT-'accounts'-GT-'{}(Lbl'Unds'AccountCellMap'Unds'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCTFROM:SortInt{}),Lbl'-LT-'balance'-GT-'{}(VarORIGFROM:SortInt{}))),Var'Unds'DotVar2:SortAccountCellMap{})),Var'Unds'Gen4:SortAccountsCell{}),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \equals{SortBool{},SortGeneratedTopCell{}}( + Lbl'Unds-GT-'Int'Unds'{}(VarVALUE:SortInt{},VarORIGFROM:SortInt{}), + \dv{SortBool{}}("true"))), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(Var'Unds'DotVar1:SortK{}),Var'Unds'Gen4:SortAccountsCell{},Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("7ecf8b0075d5324c3b741216a581b50c347b4a0fd1587f8ffa2a6815e5b190f4"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(55,10,61,35)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + +// rule ``(``(inj{Ops,KItem}(seq(`#init___SAME-NAME-DIFF-VALUE_Op_Int_Int`(ACCT,VALUE),inj{Op,Ops}(O)))),``(`.AccountCellMap`(.KList)),_DotVar0)=>``(``(inj{Op,KItem}(O)),``(`AccountCellMapItem`(``(ACCT),``(``(ACCT),``(VALUE)))),_DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f8dd11cd72735dc2bb23bf7ed0f33ffe20de7cd70f5ec80e8da5050a10545209), org.kframework.attributes.Location(Location(22,10,31,21)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + axiom{} \rewrites{SortGeneratedTopCell{}} ( + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOps{}, SortKItem{}}(Lblseq{}(Lbl'Hash'init'UndsUndsUnds'SAME-NAME-DIFF-VALUE'Unds'Op'Unds'Int'Unds'Int{}(VarACCT:SortInt{},VarVALUE:SortInt{}),inj{SortOp{}, SortOps{}}(VarO:SortOp{}))),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(Lbl'Stop'AccountCellMap{}()),Var'Unds'DotVar0:SortGeneratedCounterCell{}), + \top{SortGeneratedTopCell{}}()), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOp{}, SortKItem{}}(VarO:SortOp{}),dotk{}())),Lbl'-LT-'accounts'-GT-'{}(LblAccountCellMapItem{}(Lbl'-LT-'acctID'-GT-'{}(VarACCT:SortInt{}),Lbl'-LT-'account'-GT-'{}(Lbl'-LT-'acctID'-GT-'{}(VarACCT:SortInt{}),Lbl'-LT-'balance'-GT-'{}(VarVALUE:SortInt{})))),Var'Unds'DotVar0:SortGeneratedCounterCell{}), \top{SortGeneratedTopCell{}}())) + [UNIQUE'Unds'ID{}("f8dd11cd72735dc2bb23bf7ed0f33ffe20de7cd70f5ec80e8da5050a10545209"), org'Stop'kframework'Stop'attributes'Stop'Location{}("Location(22,10,31,21)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/llvm-backend/src/main/native/llvm-backend/test/proof/k-files/same-name-diff-value.k)")] + +// rule `AccountCellMapKey`(``(Key,_DotVar0))=>Key requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(567d52b52184cbafced994bdafc1bf4faf80806902f2d97086e1e6c70c46a1eb)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortAccountCell{}, R} ( + X0:SortAccountCell{}, + Lbl'-LT-'account'-GT-'{}(VarKey:SortAcctIDCell{},Var'Unds'DotVar0:SortBalanceCell{}) + ), + \top{R} () + )), + \equals{SortAcctIDCell{},R} ( + LblAccountCellMapKey{}(X0:SortAccountCell{}), + \and{SortAcctIDCell{}} ( + VarKey:SortAcctIDCell{}, + \top{SortAcctIDCell{}}()))) + [UNIQUE'Unds'ID{}("567d52b52184cbafced994bdafc1bf4faf80806902f2d97086e1e6c70c46a1eb")] + +// 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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(1442,8,1442,53)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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(1442,8,1442,53)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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(2322,8,2322,45)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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(2322,8,2322,45)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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(1431,8,1432,23)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + 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(1431,8,1432,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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(1443,8,1443,58)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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(1443,8,1443,58)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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(1434,5,1437,23)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)]), 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(1434,5,1437,23)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)]), 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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(1446,8,1446,28)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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(1446,8,1446,28)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule getGeneratedCounterCell(``(_Gen0,_Gen1,Cell))=>Cell requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(6aaa6e2dcc27f3f1c36a11a988ed5674f7b6892c35cde7937bcb682488aaf8e1)] + 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:SortAccountsCell{},VarCell:SortGeneratedCounterCell{}) + ), + \top{R} () + )), + \equals{SortGeneratedCounterCell{},R} ( + LblgetGeneratedCounterCell{}(X0:SortGeneratedTopCell{}), + \and{SortGeneratedCounterCell{}} ( + VarCell:SortGeneratedCounterCell{}, + \top{SortGeneratedCounterCell{}}()))) + [UNIQUE'Unds'ID{}("6aaa6e2dcc27f3f1c36a11a988ed5674f7b6892c35cde7937bcb682488aaf8e1")] + +// rule initAccountCell(.KList)=>`AccountCellMapItem`(initAcctIDCell(.KList),``(initAcctIDCell(.KList),initBalanceCell(.KList))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e2985e1a52d476f4bc396c58dae075603e63b5d27e0e6b99b19f7bd3b4b89d6d), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortAccountCellMap{},R} ( + LblinitAccountCell{}(), + \and{SortAccountCellMap{}} ( + LblAccountCellMapItem{}(LblinitAcctIDCell{}(),Lbl'-LT-'account'-GT-'{}(LblinitAcctIDCell{}(),LblinitBalanceCell{}())), + \top{SortAccountCellMap{}}()))) + [UNIQUE'Unds'ID{}("e2985e1a52d476f4bc396c58dae075603e63b5d27e0e6b99b19f7bd3b4b89d6d")] + +// rule initAccountsCell(.KList)=>``(`.AccountCellMap`(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ad313527f030a363b2a7f4ad252eb59d271c6a104646f84f634d19c3c674aacf), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortAccountsCell{},R} ( + LblinitAccountsCell{}(), + \and{SortAccountsCell{}} ( + Lbl'-LT-'accounts'-GT-'{}(Lbl'Stop'AccountCellMap{}()), + \top{SortAccountsCell{}}()))) + [UNIQUE'Unds'ID{}("ad313527f030a363b2a7f4ad252eb59d271c6a104646f84f634d19c3c674aacf")] + +// rule initAcctIDCell(.KList)=>``(#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(2e4381f040f2e618441978504ca334c7f87067148aceb9b6e559fa3c98880cf4), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortAcctIDCell{},R} ( + LblinitAcctIDCell{}(), + \and{SortAcctIDCell{}} ( + Lbl'-LT-'acctID'-GT-'{}(\dv{SortInt{}}("0")), + \top{SortAcctIDCell{}}()))) + [UNIQUE'Unds'ID{}("2e4381f040f2e618441978504ca334c7f87067148aceb9b6e559fa3c98880cf4")] + +// rule initBalanceCell(.KList)=>``(#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(bd4226b4ab10596ce04686a7ac02c1e85c44280293132a7114eedb21aaa5fdcd), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + + \top{R} () + ), + \equals{SortBalanceCell{},R} ( + LblinitBalanceCell{}(), + \and{SortBalanceCell{}} ( + Lbl'-LT-'balance'-GT-'{}(\dv{SortInt{}}("0")), + \top{SortBalanceCell{}}()))) + [UNIQUE'Unds'ID{}("bd4226b4ab10596ce04686a7ac02c1e85c44280293132a7114eedb21aaa5fdcd")] + +// 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(Init)=>``(initKCell(Init),initAccountsCell(.KList),initGeneratedCounterCell(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(287bf9aa6f9850de4009fc655775089c7d60433a1c2de665b23e1d02fde7bbf0), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortMap{}, R} ( + X0:SortMap{}, + VarInit:SortMap{} + ), + \top{R} () + )), + \equals{SortGeneratedTopCell{},R} ( + LblinitGeneratedTopCell{}(X0:SortMap{}), + \and{SortGeneratedTopCell{}} ( + Lbl'-LT-'generatedTop'-GT-'{}(LblinitKCell{}(VarInit:SortMap{}),LblinitAccountsCell{}(),LblinitGeneratedCounterCell{}()), + \top{SortGeneratedTopCell{}}()))) + [UNIQUE'Unds'ID{}("287bf9aa6f9850de4009fc655775089c7d60433a1c2de665b23e1d02fde7bbf0")] + +// rule initKCell(Init)=>``(inj{Ops,KItem}(`project:Ops`(`Map:lookup`(Init,inj{KConfigVar,KItem}(#token("$PGM","KConfigVar")))))) requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(dfe5ad42fa48753744598c5a955535c740148f40c1beef39ccf4bc8c2db662f8), initializer] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortMap{}, R} ( + X0:SortMap{}, + VarInit:SortMap{} + ), + \top{R} () + )), + \equals{SortKCell{},R} ( + LblinitKCell{}(X0:SortMap{}), + \and{SortKCell{}} ( + Lbl'-LT-'k'-GT-'{}(kseq{}(inj{SortOps{}, SortKItem{}}(Lblproject'Coln'Ops{}(kseq{}(LblMap'Coln'lookup{}(VarInit:SortMap{},inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}("$PGM"))),dotk{}()))),dotk{}())), + \top{SortKCell{}}()))) + [UNIQUE'Unds'ID{}("dfe5ad42fa48753744598c5a955535c740148f40c1beef39ccf4bc8c2db662f8")] + +// rule isAccountCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(3efd680071ad42995f20afe6c20c7b3304300692adbc35c7e5d1e9735b5e7702), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortAccountCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCell{}, SortKItem{}}(Var'Unds'Gen0:SortAccountCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("3efd680071ad42995f20afe6c20c7b3304300692adbc35c7e5d1e9735b5e7702"), owise{}()] + +// rule isAccountCell(inj{AccountCell,KItem}(AccountCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(8d7c28acece2c807d897258fec856762b12eb51a0426e7e5ff6dad87abe91b58)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCell{}, SortKItem{}}(VarAccountCell:SortAccountCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("8d7c28acece2c807d897258fec856762b12eb51a0426e7e5ff6dad87abe91b58")] + +// rule isAccountCellFragment(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fb8afa564beb87fccf17434b83b64815e6f786ae631a8eb24aa19417437bd58f), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAccountCellFragment{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellFragment{}, SortKItem{}}(Var'Unds'Gen1:SortAccountCellFragment{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("fb8afa564beb87fccf17434b83b64815e6f786ae631a8eb24aa19417437bd58f"), owise{}()] + +// rule isAccountCellFragment(inj{AccountCellFragment,KItem}(AccountCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(94e02f96d77b2e1e23b8b04c2517d1513faa6f6a8770294b02adf04f0b5c2dbd)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellFragment{}, SortKItem{}}(VarAccountCellFragment:SortAccountCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("94e02f96d77b2e1e23b8b04c2517d1513faa6f6a8770294b02adf04f0b5c2dbd")] + +// rule isAccountCellMap(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(1d73129326f7589cdd8143502b82fc0e70e5c69f1705041ffd6b9e78c54db6c9), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAccountCellMap{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellMap{}, SortKItem{}}(Var'Unds'Gen1:SortAccountCellMap{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountCellMap{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("1d73129326f7589cdd8143502b82fc0e70e5c69f1705041ffd6b9e78c54db6c9"), owise{}()] + +// rule isAccountCellMap(inj{AccountCellMap,KItem}(AccountCellMap))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(5f7ff06771465383edce3d4263fb06819f42dc9ba289d69477a7e938cbaa1251)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellMap{}, SortKItem{}}(VarAccountCellMap:SortAccountCellMap{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountCellMap{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("5f7ff06771465383edce3d4263fb06819f42dc9ba289d69477a7e938cbaa1251")] + +// rule isAccountsCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(03b755c912dd368b0a1298a83b3558c532fbaa5bfb38a1b0db42b072982aac1f), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAccountsCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCell{}, SortKItem{}}(Var'Unds'Gen1:SortAccountsCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountsCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("03b755c912dd368b0a1298a83b3558c532fbaa5bfb38a1b0db42b072982aac1f"), owise{}()] + +// rule isAccountsCell(inj{AccountsCell,KItem}(AccountsCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(8ae1d4103589cc9bab1fa5ddc6239980cc9dbb286d98e297a99cc0185424fcf5)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCell{}, SortKItem{}}(VarAccountsCell:SortAccountsCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountsCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("8ae1d4103589cc9bab1fa5ddc6239980cc9dbb286d98e297a99cc0185424fcf5")] + +// rule isAccountsCellFragment(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d2d28b1d51a5b613a2ae820d459f574313126f2d2b5e423792605d4ba392f2f2), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAccountsCellFragment{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellFragment{}, SortKItem{}}(Var'Unds'Gen1:SortAccountsCellFragment{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountsCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("d2d28b1d51a5b613a2ae820d459f574313126f2d2b5e423792605d4ba392f2f2"), owise{}()] + +// rule isAccountsCellFragment(inj{AccountsCellFragment,KItem}(AccountsCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(23a1701f3dc12af15b54306732f0c9fff894efa3a70736c8e46d50b69cc37f60)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellFragment{}, SortKItem{}}(VarAccountsCellFragment:SortAccountsCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountsCellFragment{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("23a1701f3dc12af15b54306732f0c9fff894efa3a70736c8e46d50b69cc37f60")] + +// rule isAccountsCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e6aa62b54138d2e4a87c1f1c4d913540591053187dcbf3a3134b44a6fb8ccabc), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAccountsCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellOpt{}, SortKItem{}}(Var'Unds'Gen1:SortAccountsCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAccountsCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("e6aa62b54138d2e4a87c1f1c4d913540591053187dcbf3a3134b44a6fb8ccabc"), owise{}()] + +// rule isAccountsCellOpt(inj{AccountsCellOpt,KItem}(AccountsCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(acd6ceb7765e6e974df8c1464f04abf417bde53ad449ca266a356fed3903859e)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellOpt{}, SortKItem{}}(VarAccountsCellOpt:SortAccountsCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAccountsCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("acd6ceb7765e6e974df8c1464f04abf417bde53ad449ca266a356fed3903859e")] + +// rule isAcctIDCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(77f291815ee9937f5d6890c8e17cc8ecf657244a6e091704ffa8205c1154a8c3), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortAcctIDCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCell{}, SortKItem{}}(Var'Unds'Gen1:SortAcctIDCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAcctIDCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("77f291815ee9937f5d6890c8e17cc8ecf657244a6e091704ffa8205c1154a8c3"), owise{}()] + +// rule isAcctIDCell(inj{AcctIDCell,KItem}(AcctIDCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(28181509cd74279f0e0d2a3ef06af2bee3f21a7ac78379a5ce1c6c0f01c5b012)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCell{}, SortKItem{}}(VarAcctIDCell:SortAcctIDCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAcctIDCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("28181509cd74279f0e0d2a3ef06af2bee3f21a7ac78379a5ce1c6c0f01c5b012")] + +// rule isAcctIDCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(05d54de59f3aef74397729e62c85af48c31bf0d1541cd37cb90e6d813a7d3812), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortAcctIDCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortAcctIDCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisAcctIDCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("05d54de59f3aef74397729e62c85af48c31bf0d1541cd37cb90e6d813a7d3812"), owise{}()] + +// rule isAcctIDCellOpt(inj{AcctIDCellOpt,KItem}(AcctIDCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(45a32019d48565baee3166441628fa03428e7d590e1f7c9ab74c8fdfb97b011b)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCellOpt{}, SortKItem{}}(VarAcctIDCellOpt:SortAcctIDCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisAcctIDCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("45a32019d48565baee3166441628fa03428e7d590e1f7c9ab74c8fdfb97b011b")] + +// rule isBalanceCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c3c52adfedcd66abe4d0ac88d87f4688a76d0a843b1628c1a1260cdde2006276), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortBalanceCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCell{}, SortKItem{}}(Var'Unds'Gen0:SortBalanceCell{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisBalanceCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("c3c52adfedcd66abe4d0ac88d87f4688a76d0a843b1628c1a1260cdde2006276"), owise{}()] + +// rule isBalanceCell(inj{BalanceCell,KItem}(BalanceCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(36bfd5fc03162ce627c79aeec15a2c33d60fdbd771d30cb3b29acf1444708702)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCell{}, SortKItem{}}(VarBalanceCell:SortBalanceCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisBalanceCell{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("36bfd5fc03162ce627c79aeec15a2c33d60fdbd771d30cb3b29acf1444708702")] + +// rule isBalanceCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(475c1dd66ed6c8a2c678f99ae2f231113b6e47c6e5f3e1364a8c98c8a67aee24), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen0:SortBalanceCellOpt{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCellOpt{}, SortKItem{}}(Var'Unds'Gen0:SortBalanceCellOpt{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisBalanceCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("475c1dd66ed6c8a2c678f99ae2f231113b6e47c6e5f3e1364a8c98c8a67aee24"), owise{}()] + +// rule isBalanceCellOpt(inj{BalanceCellOpt,KItem}(BalanceCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e77b5a48a52f212b0f9ea1a3e73d482ef571a2e5a483d3faabdb28ef97eafe9b)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCellOpt{}, SortKItem{}}(VarBalanceCellOpt:SortBalanceCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisBalanceCellOpt{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("e77b5a48a52f212b0f9ea1a3e73d482ef571a2e5a483d3faabdb28ef97eafe9b")] + +// 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'Gen0:SortBool{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBool{}, SortKItem{}}(Var'Unds'Gen0: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 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'Gen1:SortGeneratedCounterCell{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedCounterCell{}, SortKItem{}}(Var'Unds'Gen1: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'Gen1:SortGeneratedTopCellFragment{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortGeneratedTopCellFragment{}, SortKItem{}}(Var'Unds'Gen1: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'Gen0:SortKConfigVar{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortKConfigVar{}, SortKItem{}}(Var'Unds'Gen0: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'Gen0:SortKItem{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(Var'Unds'Gen0: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'Gen0:SortList{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortList{}, SortKItem{}}(Var'Unds'Gen0: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 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 isNoOp(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(ab5739dedcd2022d9159e6d6d5e5db36a89d6f36a5308154c62f1ba2753a020c), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortNoOp{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortNoOp{}, SortKItem{}}(Var'Unds'Gen1:SortNoOp{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisNoOp{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("ab5739dedcd2022d9159e6d6d5e5db36a89d6f36a5308154c62f1ba2753a020c"), owise{}()] + +// rule isNoOp(inj{NoOp,KItem}(NoOp))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(83f2d66158cd0aa7e48a21ac78a1010469f00293e9e15c1ad6c16d72fc938f03)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortNoOp{}, SortKItem{}}(VarNoOp:SortNoOp{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisNoOp{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("83f2d66158cd0aa7e48a21ac78a1010469f00293e9e15c1ad6c16d72fc938f03")] + +// rule isOp(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(4941790c6067010a1b2e094761ce372f5819dc38830212da75f2a12b310cb034), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortOp{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOp{}, SortKItem{}}(Var'Unds'Gen1:SortOp{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisOp{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("4941790c6067010a1b2e094761ce372f5819dc38830212da75f2a12b310cb034"), owise{}()] + +// rule isOp(inj{Op,KItem}(Op))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(e706b877f062df9800a05da60b5196592f0fb36de399fc9a577058afa2a8ba04)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOp{}, SortKItem{}}(VarOp:SortOp{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisOp{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("e706b877f062df9800a05da60b5196592f0fb36de399fc9a577058afa2a8ba04")] + +// rule isOps(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(daf9a5d6bf5fa6be0edcf99ee9cf0c4be0deb83627e1277f0a8657cb390540bf), owise] + axiom{R} \implies{R} ( + \and{R} ( + \not{R} ( + \or{R} ( + \exists{R} (Var'Unds'Gen1:SortOps{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOps{}, SortKItem{}}(Var'Unds'Gen1:SortOps{}),dotk{}()) + ), + \top{R} () + ) + )), + \bottom{R}() + ) + ), + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + VarK:SortK{} + ), + \top{R} () + ) + )), + \equals{SortBool{},R} ( + LblisOps{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("false"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("daf9a5d6bf5fa6be0edcf99ee9cf0c4be0deb83627e1277f0a8657cb390540bf"), owise{}()] + +// rule isOps(inj{Ops,KItem}(Ops))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(0cf446896156f49638f29f46d90f28e1fcc08680915f4d74027d7412649a2188)] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOps{}, SortKItem{}}(VarOps:SortOps{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBool{},R} ( + LblisOps{}(X0:SortK{}), + \and{SortBool{}} ( + \dv{SortBool{}}("true"), + \top{SortBool{}}()))) + [UNIQUE'Unds'ID{}("0cf446896156f49638f29f46d90f28e1fcc08680915f4d74027d7412649a2188")] + +// 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'Gen1:SortSet{}, + \and{R} ( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortSet{}, SortKItem{}}(Var'Unds'Gen1: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(2324,8,2324,59)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + 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(2324,8,2324,59)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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(2325,8,2325,67)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + 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(2325,8,2325,67)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `minInt(_,_)_INT-COMMON_Int_Int_Int`(I1,I2)=>I1 requires `_I2 requires `_>=Int_`(I1,I2) ensures #token("true","Bool") [UNIQUE_ID(e1effeabf96bb3a3beffd5b679ad5df95c4f8bbf42872b0793331e52a8470fb3), org.kframework.attributes.Location(Location(1440,8,1440,57)), org.kframework.attributes.Source(Source(/home/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody "requires" Bool [symbol(#ruleRequires)])] + 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(1440,8,1440,57)"), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)")] + +// rule `project:AccountCell`(inj{AccountCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(d153967a820979d557c15b49fa680fd222fe6ccbfe5017a873f73b2b67825e9e), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCell{}, SortKItem{}}(VarK:SortAccountCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountCell{},R} ( + Lblproject'Coln'AccountCell{}(X0:SortK{}), + \and{SortAccountCell{}} ( + VarK:SortAccountCell{}, + \top{SortAccountCell{}}()))) + [UNIQUE'Unds'ID{}("d153967a820979d557c15b49fa680fd222fe6ccbfe5017a873f73b2b67825e9e")] + +// rule `project:AccountCellFragment`(inj{AccountCellFragment,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(78fb3c732f4a135d6e9e7f0f16480b916ab037a2a606a2fd5852a88e3caa1a3d), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellFragment{}, SortKItem{}}(VarK:SortAccountCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountCellFragment{},R} ( + Lblproject'Coln'AccountCellFragment{}(X0:SortK{}), + \and{SortAccountCellFragment{}} ( + VarK:SortAccountCellFragment{}, + \top{SortAccountCellFragment{}}()))) + [UNIQUE'Unds'ID{}("78fb3c732f4a135d6e9e7f0f16480b916ab037a2a606a2fd5852a88e3caa1a3d")] + +// rule `project:AccountCellMap`(inj{AccountCellMap,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(18cef391126ce4015cc7e20791327206c20cbd35a88f6132ad4cccba51173906), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountCellMap{}, SortKItem{}}(VarK:SortAccountCellMap{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountCellMap{},R} ( + Lblproject'Coln'AccountCellMap{}(X0:SortK{}), + \and{SortAccountCellMap{}} ( + VarK:SortAccountCellMap{}, + \top{SortAccountCellMap{}}()))) + [UNIQUE'Unds'ID{}("18cef391126ce4015cc7e20791327206c20cbd35a88f6132ad4cccba51173906")] + +// rule `project:AccountsCell`(inj{AccountsCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(c4a91e4b698d89d48c4423dc156e52ebc1b6eaede5cd5565fef94061a9957f67), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCell{}, SortKItem{}}(VarK:SortAccountsCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountsCell{},R} ( + Lblproject'Coln'AccountsCell{}(X0:SortK{}), + \and{SortAccountsCell{}} ( + VarK:SortAccountsCell{}, + \top{SortAccountsCell{}}()))) + [UNIQUE'Unds'ID{}("c4a91e4b698d89d48c4423dc156e52ebc1b6eaede5cd5565fef94061a9957f67")] + +// rule `project:AccountsCellFragment`(inj{AccountsCellFragment,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(87b2d04db33759d68728ae729943017afc121470aaee953e1de2db565f06d708), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellFragment{}, SortKItem{}}(VarK:SortAccountsCellFragment{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountsCellFragment{},R} ( + Lblproject'Coln'AccountsCellFragment{}(X0:SortK{}), + \and{SortAccountsCellFragment{}} ( + VarK:SortAccountsCellFragment{}, + \top{SortAccountsCellFragment{}}()))) + [UNIQUE'Unds'ID{}("87b2d04db33759d68728ae729943017afc121470aaee953e1de2db565f06d708")] + +// rule `project:AccountsCellOpt`(inj{AccountsCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(33382610b7b3099507a1a3985e652f7c2a7e8c988f18ab0e872a4d789921d7e1), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAccountsCellOpt{}, SortKItem{}}(VarK:SortAccountsCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAccountsCellOpt{},R} ( + Lblproject'Coln'AccountsCellOpt{}(X0:SortK{}), + \and{SortAccountsCellOpt{}} ( + VarK:SortAccountsCellOpt{}, + \top{SortAccountsCellOpt{}}()))) + [UNIQUE'Unds'ID{}("33382610b7b3099507a1a3985e652f7c2a7e8c988f18ab0e872a4d789921d7e1")] + +// rule `project:AcctIDCell`(inj{AcctIDCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(f6fc402c8ef12ad56429a9e5d1b2aede1ac81927465aa7eda68dd0f2c015426a), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCell{}, SortKItem{}}(VarK:SortAcctIDCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAcctIDCell{},R} ( + Lblproject'Coln'AcctIDCell{}(X0:SortK{}), + \and{SortAcctIDCell{}} ( + VarK:SortAcctIDCell{}, + \top{SortAcctIDCell{}}()))) + [UNIQUE'Unds'ID{}("f6fc402c8ef12ad56429a9e5d1b2aede1ac81927465aa7eda68dd0f2c015426a")] + +// rule `project:AcctIDCellOpt`(inj{AcctIDCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(b9623357e698014054d4fd0581f8e2ce2e8f475a6b2e7138afc129dcca1fbd64), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortAcctIDCellOpt{}, SortKItem{}}(VarK:SortAcctIDCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortAcctIDCellOpt{},R} ( + Lblproject'Coln'AcctIDCellOpt{}(X0:SortK{}), + \and{SortAcctIDCellOpt{}} ( + VarK:SortAcctIDCellOpt{}, + \top{SortAcctIDCellOpt{}}()))) + [UNIQUE'Unds'ID{}("b9623357e698014054d4fd0581f8e2ce2e8f475a6b2e7138afc129dcca1fbd64")] + +// rule `project:BalanceCell`(inj{BalanceCell,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(753f1a687052f5458a872e13b41a58a87dbef3c20a35e168041811f15b6ec64f), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCell{}, SortKItem{}}(VarK:SortBalanceCell{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBalanceCell{},R} ( + Lblproject'Coln'BalanceCell{}(X0:SortK{}), + \and{SortBalanceCell{}} ( + VarK:SortBalanceCell{}, + \top{SortBalanceCell{}}()))) + [UNIQUE'Unds'ID{}("753f1a687052f5458a872e13b41a58a87dbef3c20a35e168041811f15b6ec64f")] + +// rule `project:BalanceCellOpt`(inj{BalanceCellOpt,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(13caeed4b7f7035a170e2772828bb06df4022b3dac3c871ca4f50e47544f4425), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortBalanceCellOpt{}, SortKItem{}}(VarK:SortBalanceCellOpt{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortBalanceCellOpt{},R} ( + Lblproject'Coln'BalanceCellOpt{}(X0:SortK{}), + \and{SortBalanceCellOpt{}} ( + VarK:SortBalanceCellOpt{}, + \top{SortBalanceCellOpt{}}()))) + [UNIQUE'Unds'ID{}("13caeed4b7f7035a170e2772828bb06df4022b3dac3c871ca4f50e47544f4425")] + +// 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: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: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:NoOp`(inj{NoOp,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(52e932a6815383e4082016f3ac1bb74065f94ca7c369d721f00af576cb85e57e), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortNoOp{}, SortKItem{}}(VarK:SortNoOp{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortNoOp{},R} ( + Lblproject'Coln'NoOp{}(X0:SortK{}), + \and{SortNoOp{}} ( + VarK:SortNoOp{}, + \top{SortNoOp{}}()))) + [UNIQUE'Unds'ID{}("52e932a6815383e4082016f3ac1bb74065f94ca7c369d721f00af576cb85e57e")] + +// rule `project:Op`(inj{Op,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(8c952458880ec6ee2b83dcff597d3fc2fa246995dc8552e96954833515c40bdf), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOp{}, SortKItem{}}(VarK:SortOp{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortOp{},R} ( + Lblproject'Coln'Op{}(X0:SortK{}), + \and{SortOp{}} ( + VarK:SortOp{}, + \top{SortOp{}}()))) + [UNIQUE'Unds'ID{}("8c952458880ec6ee2b83dcff597d3fc2fa246995dc8552e96954833515c40bdf")] + +// rule `project:Ops`(inj{Ops,KItem}(K))=>K requires #token("true","Bool") ensures #token("true","Bool") [UNIQUE_ID(fbe4201fd756a10d87f9ea9c8e8521f42269814d9fdacb4cf4afb75dddc4ed26), projection] + axiom{R} \implies{R} ( + \and{R}( + \top{R}(), + \and{R} ( + \in{SortK{}, R} ( + X0:SortK{}, + kseq{}(inj{SortOps{}, SortKItem{}}(VarK:SortOps{}),dotk{}()) + ), + \top{R} () + )), + \equals{SortOps{},R} ( + Lblproject'Coln'Ops{}(X0:SortK{}), + \and{SortOps{}} ( + VarK:SortOps{}, + \top{SortOps{}}()))) + [UNIQUE'Unds'ID{}("fbe4201fd756a10d87f9ea9c8e8521f42269814d9fdacb4cf4afb75dddc4ed26")] + +// 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/robertorosmaninho/rv/k/k-distribution/target/release/k/include/kframework/builtin/domains.md)), org.kframework.definition.Production(syntax #RuleContent ::= #RuleBody [symbol(#ruleNoConditions)])] + 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/robertorosmaninho/rv/k/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),`_<