This is my generated k-prelude.kore file

require "builtins/builtins.k"

module K-TECHNIQUE
/*  all basic K syntax is in the SDF grammar directly, */
/*  but also needs to be defined in K - except for */
/*  a few things added by compiler passes. */
/*  Unfortunately, FlattenModules explicitly ignores */
/*  includes of K-TECHNIQUE and some other core modules, */
/*  so we have to declare things like isSet in less obvious places */

endmodule
module K-LISTK-EXTRAS
  imports K-TECHNIQUE
  imports K-EQUAL-HOOKS
  syntax Bool ::=K "inKList" KList [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((18,19,18,46)),  cons(Bool1267Syn),  prefixlabel(_inKList_),  klabel('_inKList_), kore]
  syntax Bool ::=K "#inKList" KList [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((19,19,19,47)),  cons(Bool1268Syn),  prefixlabel(_#inKList_),  klabel('_#inKList_), kore]
  rule { '_inKList_(K:K ,  2KLabel KList(L:KList)(.KList):KItem):KItem => '_==K_('_#inKList_(K:K ,  2KLabel KList(L:KList)(.KList):KItem):KItem , true(.KList):KItem):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((20,3,20,51)), kore]
  rule { '_#inKList_(K:K ,  2KLabel KList(_:KList , K:K , _:KList)(.KList):KItem):KItem => true(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((21,3,21,37)), kore]

endmodule
module K-MAP-EXTRAS
  imports K-TECHNIQUE
  imports K-SET-EXTRAS
  imports BOOL-HOOKS
  imports K-EQUAL-HOOKS
  syntax K ::=Map "(" K ")" [ function,  klabel(deprecatedMapLookup),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((30,16,30,69)),  cons(K1269Syn),  prefixlabel(_(_)), kore]
  rule { deprecatedMapLookup( 2KLabel KItem('_Map_(_:Map , '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem):KItem)(.KList):KItem , K1:K):KItem => K2:K }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((31,3,31,34)), kore]
  syntax Map ::=Map "[" "undef" "/" KList "]" [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((33,18,33,58)),  cons(Map1270Syn),  prefixlabel(_[undef/_]),  klabel('_[undef/_]), kore]
  syntax Map ::="Map" "(" KList "|->" KList ")" [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((35,18,35,61)),  cons(Map1272Syn),  prefixlabel(Map(_|->_)),  klabel('Map(_|->_)), kore]
  rule '_Map_('Map`(_|->_`)( [ { K1:K => .KList }
 , _:KList ]  ,  [ { K2:K => .KList }
 , _:K , _:KList ] ):Map , '_Map_({ '.MyMap(.KList):KItem => '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem }
 , '.MyMap(.KList):KItem):KItem):KItem [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((36,3,36,90)), kore]
  rule '_Map_('Map`(_|->_`)( [ { K1:K => .KList }
 , _:KList ]  , K2:K):Map , '_Map_({ '.MyMap(.KList):KItem => '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem }
 , '.MyMap(.KList):KItem):KItem):KItem [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((37,3,37,57)), kore]
  rule { 'Map`(_|->_`)( [ .KList ]  , _:KList):Map => '.MyMap(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((38,3,38,29)), kore]
  syntax Map ::=Map "[" KList "/" KList "]" [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((40,18,40,56)),  cons(Map1273Syn),  prefixlabel(_[_/_]),  klabel('_[_/_]), kore]
  rule '_[_/_]({ M:Map => '_[_/_]('_[_/_](M:Map , K2:K , K1:K):Map , K2':K , K1':K):Map }
 ,  [ { K2:K , K2':K => .KList }
 , _:KList ]  ,  [ { K1:K , K1':K => .KList }
 , _:KList ] ):Map [ structural,  anywhere,  nojava,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((41,3,43,33)), kore]
  rule { '_[_/_](M:Map ,  [ .KList ]  ,  [ .KList ] ):Map => M:Map }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((44,3,45,25)), kore]
  rule { '_[_/_]('_Map_(M:Map , '_Map_('_|->_(K1:K , _:K):KItem , '.MyMap(.KList):KItem):KItem):KItem , K2:K , K1:K):Map => '_Map_(M:Map , '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((47,3,48,26)), kore]
  rule { '_[_/_](M:Map , K2:K , K1:K):Map => '_Map_(M:Map , '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem):KItem }
 requires 'notBool_(inSet(K1:K ,  2KLabel Set('keys_(M:Map):Set)(.KList):KItem):KItem):KItem [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((49,3,50,54)), kore]
  rule { '_[undef/_](M:Map ,  [ K:K , Kl:KList ] ):Map => '_[undef/_]('_[undef/_](M:Map , K:K):Map , Kl:KList):Map }
 requires '_=/=KList_( 2KLabel KList(Kl:KList)(.KList):KItem ,  2KLabel KList(.KList)(.KList):KItem):KItem [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((52,3,52,107)), kore]
  rule { '_[undef/_](M:Map ,  [ .KList ] ):Map => M:Map }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((53,3,53,55)), kore]
  rule { '_[undef/_]('_Map_(M:Map , '_Map_('_|->_(K:K , _:K):KItem , '.MyMap(.KList):KItem):KItem):KItem , K:K):Map => M:Map }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((54,3,54,62)), kore]
  syntax Map ::=Map "[" Map "]" [ function,  cons(Map1UpdateMapWithMapSyn),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((56,18,56,76)),  prefixlabel(_[_]),  klabel('_[_]), kore]
  rule { '_[_](M:Map , '_Map_(M':Map , '_Map_('_|->_(K1:K , K2:K):KItem , '.MyMap(.KList):KItem):KItem):KItem):Map => '_[_]('_[_/_](M:Map , K2:K , K1:K):Map , M':Map):Map }
 [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((57,3,57,63)), kore]
  rule { '_[_](M:Map , '.MyMap(.KList):KItem):Map => M:Map }
 [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((58,3,58,36)), kore]
/*   syntax KList ::= Map "(" KList ")" */
/*   rule Map:Map((K1:K,,K2:K,,Ks:KList)) */
/*     => Map(K1),,Map(K2),,Map(Ks) [structural] */
/*   rule Map:Map(.KList) => .KList [structural] */
  syntax Set ::="keys" Map [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((65,24,65,45)),  cons(Set1274Syn),  prefixlabel(keys_),  klabel('keys_), kore]
  rule { 'keys_('.MyMap(.KList):KItem):Set => '.MySet(.KList):KItem }
 [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((67,3,67,31)), kore]
  rule '_Set_('keys_('_Map_({ '_Map_('_|->_(K:K , _:K):KItem , '.MyMap(.KList):KItem):KItem => '.MyMap(.KList):KItem }
 , '_Map_(_:Map , '.MyMap(.KList):KItem):KItem):KItem):Set , '_Set_({ '.MySet(.KList):KItem => '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem }
 , '.MySet(.KList):KItem):KItem):KItem [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((68,3,68,65)), kore]
  syntax Set ::="values" Map [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((70,24,70,47)),  cons(Set1275Syn),  prefixlabel(values_),  klabel('values_), kore]
  rule { 'values_('.MyMap(.KList):KItem):Set => '.MySet(.KList):KItem }
 [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((72,3,72,33)), kore]
  rule '_Set_('values_('_Map_({ '_Map_('_|->_(_:K , K:K):KItem , '.MyMap(.KList):KItem):KItem => '.MyMap(.KList):KItem }
 , '_Map_(_:Map , '.MyMap(.KList):KItem):KItem):KItem):Set , '_Set_({ '.MySet(.KList):KItem => '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem }
 , '.MySet(.KList):KItem):KItem):KItem [ structural,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((73,3,73,68)), kore]
  syntax Bool ::="$hasMapping" "(" Map "," K ")" [ function,  maudeop($hasMapping),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((75,19,75,83)),  cons(Bool1276Syn),  prefixlabel($hasMapping(_,_)),  klabel('$hasMapping(_,_)), kore]
  syntax Bool ::="#hasMapping" "(" Map "," K ")" [ function,  maudeop(#hasMapping),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((76,19,76,84)),  cons(Bool1277Syn),  prefixlabel(#hasMapping(_,_)),  klabel('#hasMapping(_,_)), kore]
  rule { '$hasMapping`(_,_`)( 2KLabel Map(M:Map)(.KList):KItem , K:K):KItem => '_==K_('#hasMapping`(_,_`)( 2KLabel Map(M:Map)(.KList):KItem , K:K):KItem , true(.KList):KItem):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((77,3,77,58)), kore]
  rule { '#hasMapping`(_,_`)( 2KLabel KItem('_Map_(_:Map , '_Map_('_|->_(K:K , _:K):KItem , '.MyMap(.KList):KItem):KItem):KItem)(.KList):KItem , K:K):KItem => true(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((79,3,79,47)), kore]
/*  The following are used in pattern-matching.k */
  syntax K ::="#map" "(" Map ")" [ klabel('#map),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((84,16,84,24)),  cons(K1278Syn),  prefixlabel(#map(_)), kore]
  syntax Bool ::="#isMapInK" "(" K ")" [ function,  klabel('#isMapInK),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((85,19,85,45)),  cons(Bool1279Syn),  prefixlabel(#isMapInK(_)), kore]
  syntax Map ::="#getMapFromK" "(" K ")" [ function,  klabel('#getMapFromK),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((86,19,86,45)),  cons(Map1280Syn),  prefixlabel(#getMapFromK(_)), kore]
  rule { '#isMapInK('#map( 2KLabel Map(_:Map)(.KList):KItem):KItem):KItem => true(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((87,3,87,33)), kore]
  rule { '#getMapFromK('#map( 2KLabel Map(M:Map)(.KList):KItem):KItem):Map => M:Map }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((88,3,88,37)), kore]

endmodule
module K-SET-EXTRAS
  imports K-TECHNIQUE
  imports BOOL-HOOKS
  imports K-EQUAL-HOOKS
  syntax KLabel ::="isSet" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((97,21,97,27)), kore]
/* 	syntax Set ::= "Set" KList */
  syntax Set ::=Set "-Set" Set [ function,  latex({#1}-_{\it Set}{#2}),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((100,24,100,77)),  cons(Set1282Syn),  prefixlabel(_-Set_),  klabel('_-Set_), kore]
  rule { '_-Set_(S1:Set , '_Set_(SI1:SetItem , '_Set_(SI2:SetItem , '_Set_(S2:Set , '.MySet(.KList):KItem):KItem):KItem):KItem):Set => '_-Set_('_-Set_('_-Set_(S1:Set , SI1:SetItem):Set , SI2:SetItem):Set , S2:Set):Set }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((101,3,102,39)), kore]
  rule { '_-Set_(S1:Set , '.MySet(.KList):KItem):Set => S1:Set }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((103,3,103,26)), kore]
  rule { '_-Set_('_Set_(SI:SetItem , '_Set_(S:Set , '.MySet(.KList):KItem):KItem):KItem , SI:SetItem):Set => S:Set }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((104,3,104,38)), kore]
  rule { '_-Set_(S:Set , SI:SetItem):Set => S:Set }
 requires '_==Bool_(kInSet( 2KLabel Set(SI:SetItem)(.KList):KItem ,  2KLabel Set(S:Set)(.KList):KItem):KItem , false(.KList):KItem):KItem [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((105,3,105,59)), kore]
/*   [owise] */
  syntax Bool ::=K "in" Set [ function,  klabel(inSet),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((107,25,107,62)),  cons(Bool1283Syn),  prefixlabel(_in_), kore]
     | SetItem "in" Set [ function,  klabel(kInSet),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((108,33,108,77)),  cons(Bool1284Syn),  prefixlabel(_in_), kore]
     | K "#inSet" Set [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((109,33,109,59)),  cons(Bool1285Syn),  prefixlabel(_#inSet_),  klabel('_#inSet_), kore]
  rule { kInSet( 2KLabel KItem('_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem)(.KList):KItem ,  2KLabel Set(S:Set)(.KList):KItem):KItem => inSet(K:K ,  2KLabel Set(S:Set)(.KList):KItem):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((110,4,110,62)), kore]
  rule { inSet(K:K ,  2KLabel Set(S:Set)(.KList):KItem):KItem => '_==K_('_#inSet_(K:K ,  2KLabel Set(S:Set)(.KList):KItem):KItem , true(.KList):KItem):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((111,4,112,27)), kore]
  rule { '_#inSet_(K:K ,  2KLabel KItem('_Set_(_:Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem)(.KList):KItem):KItem => true(.KList):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((113,4,114,27)), kore]
  rule { '_-Set_('_Set_(S1:Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem , '_Set_(S2:Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem):Set => '_-Set_(S1:Set , '_Set_(S2:Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem):Set }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((116,4,116,108)), kore]
  rule { '_-Set_('_Set_(S1:Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem , S2:Set):Set => '_Set_('_-Set_(S1:Set , S2:Set):Set , '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem):KItem }
 requires 'notBool_(inSet(K:K ,  2KLabel Set(S2:Set)(.KList):KItem):KItem):KItem [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((117,4,117,114)), kore]
  rule { '_-Set_('.MySet(.KList):KItem , _:Set):Set => '.MySet(.KList):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((118,4,118,54)), kore]
  syntax Set ::="intersectSet" "(" Set "," Set ")" [ function,  klabel('intersectSet),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((121,18,121,50)),  cons(Set1286Syn),  prefixlabel(intersectSet(_,_)), kore]
  rule { 'intersectSet(A:Set , B:Set):Set => '_-Set_(A:Set , '_-Set_(A:Set , B:Set):Set):Set }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((122,3,122,54)), kore]
  syntax Bool ::="isEmptySet" "(" Set ")" [ function,  klabel('isEmptySet),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((124,19,124,44)),  cons(Bool1287Syn),  prefixlabel(isEmptySet(_)), kore]
  rule { 'isEmptySet( 2KLabel Set(A:Set)(.KList):KItem):KItem => '_==Set_( 2KLabel Set(A:Set)(.KList):KItem ,  2KLabel KItem('.MySet(.KList):KItem)(.KList):KItem):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((125,3,125,42)), kore]
  syntax KLabel ::="#set" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((127,21,127,26)), kore]
  syntax K ::="Set2KTerm" "(" Set ")" [ function,  klabel('Set2KTerm),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((129,16,129,47)),  cons(K1288Syn),  prefixlabel(Set2KTerm(_)), kore]
  rule { 'Set2KTerm( 2KLabel Set(S:Set)(.KList):KItem):KItem => 'Set2KTermAcc( 2KLabel Set(S:Set)(.KList):KItem , #set(.KList):K):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((130,3,130,56)), kore]
  syntax K ::="Set2KTermAcc" "(" Set "," K ")" [ function,  klabel('Set2KTermAcc),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((132,16,132,47)),  cons(K1289Syn),  prefixlabel(Set2KTermAcc(_,_)), kore]
  rule 'Set2KTermAcc( 2KLabel KItem('_Set_({ '_Set_('MySetItem(K:K):KItem , '.MySet(.KList):KItem):KItem => '.MySet(.KList):KItem }
 , '_Set_(_:Set , '.MySet(.KList):KItem):KItem):KItem)(.KList):KItem , _:KLabel(_:KList , { .KList => K:K }
):K):KItem [ nojava,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((133,3,133,74)), kore]
  rule { 'Set2KTermAcc( 2KLabel KItem('.MySet(.KList):KItem)(.KList):KItem , K:K):KItem => K:K }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((134,3,134,35)), kore]

endmodule
module K-LIST-EXTRAS
  imports K-TECHNIQUE
/* imports BOOL */
  imports INT-HOOKS
/* 	syntax List ::= "List" KList */
  syntax Int ::="lengthList" List [ function,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((149,24,149,51)),  cons(Int1290Syn),  prefixlabel(lengthList_),  klabel('lengthList_), kore]
  rule { 'lengthList_( 2KLabel KItem('_List_(_:ListItem , '_List_(L:List , '.MyList(.KList):KItem):KItem):KItem)(.KList):KItem):KItem => '_+Int_(1(.KList):KItem , 'lengthList_( 2KLabel List(L:List)(.KList):KItem):KItem):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((151,4,151,86)), kore]
  rule { 'lengthList_( 2KLabel KItem('.MyList(.KList):KItem)(.KList):KItem):KItem => 0(.KList):KItem }
 [ structural,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((152,4,152,52)), kore]
  rule { isKResult(_:KItem , K:K , KL:KList):K => isKResult(K:K , KL:KList):K }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((153,4,153,63)), kore]
  rule { isKResult(.KList):K => true(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((154,4,154,33)), kore]

endmodule
module K-RESULT
  imports K-TECHNIQUE
  imports BOOL-HOOKS
  syntax K ::=KResult [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((161,22,161,28)), kore]
  syntax KLabel ::="isKResult" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((162,27,162,37)), kore]
/* op .KList : -> List{KResult} [ditto metadata "latex=(renameTo \\ensuremath{\\dotCt{List\\{K\\}}})"] . */

endmodule
module K-WRAPPERS-LABELS
  imports K-TECHNIQUE
  syntax KLabel ::="KLabel2KLabel" KLabel [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((173,27,173,48)),  cons(KLabel1292Syn),  prefixlabel(KLabel2KLabel_),  klabel(KLabel2KLabel_), kore]
     | "CellLabel2KLabel" CellLabel [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((174,43,174,70)),  cons(KLabel1293Syn),  prefixlabel(CellLabel2KLabel_),  klabel(CellLabel2KLabel_), kore]
     | "KList2KLabel" KList [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((175,43,175,62)),  cons(KLabel1294Syn),  prefixlabel(KList2KLabel_),  klabel(KList2KLabel_), kore]
     | "Bag2KLabel" Bag [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((176,43,176,58)),  cons(KLabel1295Syn),  prefixlabel(Bag2KLabel_),  klabel(Bag2KLabel_), kore]
     | "Set2KLabel" Set [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((177,43,177,58)),  cons(KLabel1296Syn),  prefixlabel(Set2KLabel_),  klabel(Set2KLabel_), kore]
     | "List2KLabel" List [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((178,43,178,60)),  cons(KLabel1297Syn),  prefixlabel(List2KLabel_),  klabel(List2KLabel_), kore]
     | "Map2KLabel" Map [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((179,43,179,58)),  cons(KLabel1298Syn),  prefixlabel(Map2KLabel_),  klabel(Map2KLabel_), kore]
     | "wrap-with" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((180,43,180,53)), kore]
  rule { isSet(Set2KLabel_(_:Set):KLabel(.KList):K):K => true(.KList):KItem }
 [ predicate,  anywhere,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((184,3,184,64)), kore]

endmodule
module K-DESTRUCTORS
  syntax KLabel ::="getKLabel" K [ function,  hook(MetaK:getKLabel_),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((189,21,189,69)),  cons(KLabel1299Syn),  prefixlabel(getKLabel_),  klabel(getKLabel_), kore]
  rule { getKLabel_(L:KLabel(_:KList):K):KLabel(.KList):KItem => L:KLabel(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((190,3,190,40)), kore]

endmodule
module K-WRAPPERS
  imports K-TECHNIQUE
/*  not used anymore */
/* 	syntax K ::= KLabel2K (KLabel)		[klabel('KLabel2K_)] */
/* 			   | Celllabel2K (CellLabel)[klabel('Celllabel2K_)] */
/* 			   | KList2K (KList)		[klabel('KList2K_)] */
/* 			   | Set2K (Set)			[klabel('Set2K_)] */
/* 			   | Bag2K (Bag)			[klabel('Bag2K_)] */
/* 			   | List2K (List)			[klabel('List2K_)] */
/* 			   | Map2K (Map)			[klabel('Map2K_)] */

endmodule
module K-EVAL
  imports K-TECHNIQUE
  syntax Bag ::="#eval" Map [ cons(Bag1EvalSyn),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((208,18,208,57)),  prefixlabel(#eval_),  klabel('#eval_), kore]
  syntax Bag ::="#evalHelper" Map [ cons(Bag1EvalHelperSyn),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((209,18,209,63)),  prefixlabel(#evalHelper_),  klabel('#evalHelper_), kore]

endmodule
module K-BUILTINS
  syntax KLabel ::="#" K [ builtinWrapper,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((213,22,213,43)),  cons(KLabel1300Syn),  prefixlabel(#_),  klabel(#_), kore]

endmodule
module K-FRESH
  imports K-TECHNIQUE
  syntax Bool ::="fresh" "(" K ")" [ cons(Bool1FreshSyn),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((219,19,219,58)),  prefixlabel(fresh(_)),  klabel('fresh(_)), kore]

endmodule
module K-FREZERS
  imports K-TECHNIQUE
  syntax KLabel ::="#freezer" K [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((224,21,224,32)),  cons(KLabel1302Syn),  prefixlabel(#freezer_),  klabel(#freezer_), kore]
  syntax KLabel ::="heat" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((225,21,225,26)), kore]
     | "heated" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((225,30,225,37)), kore]
     | "redex" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((225,41,225,47)), kore]
     | "cool" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((225,51,225,56)), kore]
  rule { heat(heated(K:K):K):K => K:K }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((227,3,227,29)), kore]
  rule { heat(heated(_:KList , K:K , _:KList):K):K => K:K }
 [ heat-choice,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((228,3,229,18)), kore]
  rule heat({ redex(_:K , K:K , KL:KList):K => K:K , KL:KList }
 , _:KList):K [ owise,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((231,3,232,11)), kore]
  rule heat({ redex(K:K):K => .KList }
 , _:KList , heated(_:KList , { .KList => K:K }
):K):K [ owise,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((233,3,234,11)), kore]
  rule { cool(K:K):K => K:K }
 [ owise,  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((236,3,236,29)), kore]

endmodule
module DEFAULT-CONFIGURATION
  imports K-TECHNIQUE
  configuration <k> $PGM:K </k> [ location((241,17,241,32)),  filename(/home/qangel/project/k-master/include/k-prelude.k), kore]

endmodule
module K-TOKENS
  imports K-TECHNIQUE
  syntax KLabel ::="#token" [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((246,21,246,28)), kore]
  syntax Bool ::="isToken" "(" K ")" [ predicate,  hook(#PREDICATE:isToken),  klabel('isToken),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((247,19,247,66)),  cons(Bool1303Syn),  prefixlabel(isToken(_)), kore]
  rule { 'isToken(#token(_:KList):K):KItem => true(.KList):KItem }
 [ filename(/home/qangel/project/k-master/include/k-prelude.k),  location((248,3,248,33)), kore]
/* [klabel(isBuiltin), predicate, hook(#PREDICATE:isBuiltin)] */
  syntax Bool ::="isBuiltin" "(" K ")" [ prefixlabel(isBuiltin),  klabel(isBuiltin),  predicate,  hook(#PREDICATE:isBuiltin),  filename(/home/qangel/project/k-master/include/k-prelude.k),  location((249,19,251,84)),  cons(Bool1304Syn), kore]

endmodule
module K
  imports K-TECHNIQUE
  imports DEFAULT-CONFIGURATION
  imports K-WRAPPERS
  imports K-WRAPPERS-LABELS
  imports K-BUILTINS
  imports K-RESULT
/*  to express results syntactically */
/*  imports K-RULES              // to write k rules with in-place rewriting */
  imports K-EVAL
/*  imports K-CONTEXTS */
  imports K-DESTRUCTORS
/*  defines getKLabel and getKList for K */
/* imports K-EXTRAS                // defines a KLabel substitution */
  imports K-FREZERS
  imports K-FRESH
  imports K-LISTK-EXTRAS
  imports K-LIST-EXTRAS
  imports K-MAP-EXTRAS
/*  operations on Maps */
  imports K-SET-EXTRAS
/*  operations on Sets */
  imports K-TOKENS
/* imports K-LATEX */

endmodule