Skip to content

Instantly share code, notes, and snippets.

@dwightguth

dwightguth/imp.kore

Last active May 31, 2018 19:12
Show Gist options
  • Save dwightguth/d14a57ad9eded9f021b1077f55200344 to your computer and use it in GitHub Desktop.
Save dwightguth/d14a57ad9eded9f021b1077f55200344 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
imp.kore
[]
module BASIC-K
sort K{} []
sort KItem{} []
endmodule []
module KSEQ
import BASIC-K []
symbol kseq{}(KItem{}, K{}) : K{} []
symbol append{}(K{}, K{}) : K{} []
symbol dotk{}() : K{} []
axiom{R}
\equals{K{},R}(
append{}(dotk{}(),K2:K{}),
K2:K{})
[]
axiom{R}
\equals{K{},R}(
append{}(kseq{}(K1:KItem{},K2:K{}),K3:K{}),
kseq{}(K1:KItem{},append{}(K2:K{},K3:K{})))
[]
endmodule []
module INJ
symbol inj{From,To}(From) : To []
axiom{S1,S2,S3,R}
\equals{S3,R}(
inj{S2,S3}(inj{S1,S2}(T:S1)),
inj{S1,S3}(T:S1))
[]
endmodule []
module K
import KSEQ []
import INJ []
endmodule []
module IMP
// imports
import K []
// sorts
sort List{} []
sort TCellFragment{} []
hooked-sort String{} []
sort StateCell{} []
sort KConfigVar{} []
sort TCell{} []
sort Ids{} []
sort BExp{} []
sort StateCellOpt{} []
sort Id{} []
sort Cell{} []
hooked-sort Bool{} []
sort KCell{} []
sort KResult{} []
sort Map{} []
sort KCellOpt{} []
sort Stmt{} []
hooked-sort Int{} []
hooked-sort Float{} []
sort Pgm{} []
sort Block{} []
sort Set{} []
sort AExp{} []
// symbols
symbol LblinitKCell{}(Map{}) : KCell{} []
symbol Lbl'Stop'Set{}() : Set{} []
hooked-symbol LblInt2String{}(Int{}) : String{} []
hooked-symbol Lblkeys'Unds'list'LParUndsRParUnds'MAP'UndsUnds'Map{}(Map{}) : List{} []
hooked-symbol Lbl'Unds-GT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
hooked-symbol Lbl'UndsEqlsEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
hooked-symbol Lbl'Unds'xorInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
symbol Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(BExp{}) : BExp{} []
hooked-symbol Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
symbol LblisKResult{}(K{}) : Bool{} []
symbol Lbl'Unds'dividesInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
hooked-symbol LblchrChar{}(Int{}) : String{} []
hooked-symbol Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
hooked-symbol LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Int{} []
hooked-symbol LblreplaceFirst'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(String{}, String{}, String{}) : String{} []
hooked-symbol Lbl'Unds-LT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
symbol Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(Ids{}, Stmt{}) : Pgm{} []
hooked-symbol Lbl'UndsEqlsEqls'K'Unds'{}(K{}, K{}) : Bool{} []
hooked-symbol LblListItem{}(K{}) : List{} []
symbol LblisStateCellOpt{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds-LT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
hooked-symbol LblintersectSet{}(Set{}, Set{}) : Set{} []
symbol LblisKCellOpt{}(K{}) : Bool{} []
symbol Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(Id{}, AExp{}) : Stmt{} []
symbol LblisBool{}(K{}) : Bool{} []
hooked-symbol Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(Map{}, K{}) : Map{} []
hooked-symbol Lbl'UndsAnd'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : String{} []
hooked-symbol LblremoveAll{}(Map{}, Set{}) : Map{} []
symbol Lbl'-LT-'T'-GT-'{}(KCell{}, StateCell{}) : TCell{} []
hooked-symbol Lbl'Unds-LT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
symbol LblisTCell{}(K{}) : Bool{} []
hooked-symbol LblSet'Coln'in{}(K{}, Set{}) : Bool{} []
hooked-symbol Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
hooked-symbol LblsrandInt{}(Int{}) : K{} []
symbol LblisIds{}(K{}) : Bool{} []
hooked-symbol LblrandInt{}(Int{}) : Int{} []
symbol LblisStmt{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
hooked-symbol LblMap'Coln'choice{}(Map{}) : K{} []
symbol Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(AExp{}, AExp{}) : BExp{} []
symbol Lbl'Unds'Map'Unds'{}(Map{}, Map{}) : Map{} []
symbol Lbl'Unds'List'Unds'{}(List{}, List{}) : List{} []
hooked-symbol LblSet'Coln'choice{}(Set{}) : K{} []
symbol LblisBExp{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds'divInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'UndsXor-Perc'Int'UndsUndsUnds'INT'UndsUnds'Int'Unds'Int'Unds'Int{}(Int{}, Int{}, Int{}) : Int{} []
hooked-symbol Lbl'UndsPerc'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol LblreplaceAll'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(String{}, String{}, String{}) : String{} []
symbol Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K{}) : KItem{} []
hooked-symbol Lbl'UndsEqlsSlshEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
symbol Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(Int{}) : AExp{} []
hooked-symbol Lblsize{}(Set{}) : Int{} []
symbol Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(BExp{}, Block{}) : Stmt{} []
symbol Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(BExp{}, BExp{}) : BExp{} []
hooked-symbol LblfindChar{}(String{}, String{}, Int{}) : Int{} []
symbol LblisK{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds'inList'Unds'{}(K{}, List{}) : Bool{} []
symbol Lbl'Stop'List{}() : List{} []
hooked-symbol Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(String{}, String{}, String{}, Int{}) : String{} []
symbol LblisMap{}(K{}) : Bool{} []
symbol LblnoStateCell{}() : StateCellOpt{} []
symbol LblisTCellFragment{}(K{}) : Bool{} []
symbol Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K{}) : KItem{} []
hooked-symbol Lbl'Tild'Int'UndsUnds'INT'UndsUnds'Int{}(Int{}) : Int{} []
hooked-symbol Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{S0}(Bool{}, S0, S0) : S0 []
hooked-symbol Lbl'Unds-GT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
hooked-symbol LblnewUUID'Unds'STRING'Unds'{}() : String{} []
hooked-symbol Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'MAP'UndsUnds'Map'Unds'K'Unds'K{}(Map{}, K{}, K{}) : Map{} []
hooked-symbol LblString2Base{}(String{}, Int{}) : Int{} []
symbol LblisId{}(K{}) : Bool{} []
hooked-symbol LbllengthString{}(String{}) : Int{} []
hooked-symbol Lbl'Unds-LT--LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'UndsEqlsSlshEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
symbol LblinitTCell{}(Map{}) : TCell{} []
symbol LblisSet{}(K{}) : Bool{} []
hooked-symbol Lbl'UndsEqlsEqls'Int'Unds'{}(Int{}, Int{}) : Bool{} []
symbol LblfreshId{}(Int{}) : Id{} []
hooked-symbol LblupdateMap{}(Map{}, Map{}) : Map{} []
hooked-symbol LblrfindChar{}(String{}, String{}, Int{}) : Int{} []
hooked-symbol LblMap'Coln'lookup{}(Map{}, K{}) : K{} []
symbol LblisString{}(K{}) : Bool{} []
hooked-symbol Lblvalues{}(Map{}) : List{} []
hooked-symbol Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
hooked-symbol Lbl'Unds'modInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'Unds'-Map'UndsUnds'MAP'UndsUnds'Map'Unds'Map{}(Map{}, Map{}) : Map{} []
symbol LblisInt{}(K{}) : Bool{} []
hooked-symbol LblfindString{}(String{}, String{}, Int{}) : Int{} []
symbol Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(Id{}, Ids{}) : Ids{} []
hooked-symbol LblString2Float{}(String{}) : Float{} []
hooked-symbol Lbl'UndsPipe'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
symbol LblisCell{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
hooked-symbol LblString2Id{}(String{}) : Id{} []
symbol Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(K{}, K{}) : KItem{} []
hooked-symbol LblList'Coln'get{}(List{}, Int{}) : K{} []
symbol Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(AExp{}, AExp{}) : AExp{} []
hooked-symbol LblsizeMap{}(Map{}) : Int{} []
hooked-symbol LblId2String{}(Id{}) : String{} []
symbol Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K{}) : KItem{} []
hooked-symbol LblnotBool'Unds'{}(Bool{}) : Bool{} []
hooked-symbol LblList'Coln'range{}(List{}, Int{}, Int{}) : List{} []
symbol Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(AExp{}, AExp{}) : AExp{} []
symbol Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'UndsQuotRBraUnds'Ids{}() : Ids{} []
symbol Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(Stmt{}, Stmt{}) : Stmt{} []
symbol Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K{}) : KItem{} []
hooked-symbol Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
hooked-symbol Lbl'Unds-LT-Eqls'Map'UndsUnds'MAP'UndsUnds'Map'Unds'Map{}(Map{}, Map{}) : Bool{} []
hooked-symbol LblrfindString{}(String{}, String{}, Int{}) : Int{} []
symbol Lbl'-LT-'state'-GT-'{}(Map{}) : StateCell{} []
hooked-symbol LblFloat2String{}(Float{}) : String{} []
hooked-symbol Lbl'Unds-GT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(String{}, String{}) : Bool{} []
symbol LblisStateCell{}(K{}) : Bool{} []
symbol Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}() : KItem{} []
hooked-symbol Lbl'Unds-GT--GT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'UndsPipe'-'-GT-Unds'{}(K{}, K{}) : Map{} []
hooked-symbol LblMap'Coln'lookupOrDefault{}(Map{}, K{}, K{}) : K{} []
symbol LblisList{}(K{}) : Bool{} []
hooked-symbol Lbl'UndsStar'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'Unds-GT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
hooked-symbol LblcategoryChar{}(String{}) : String{} []
hooked-symbol Lbl'UndsSlsh'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol LblBase2String{}(Int{}, Int{}) : String{} []
hooked-symbol LblSetItem{}(K{}) : Set{} []
symbol LblinitStateCell{}() : StateCell{} []
symbol Lbl'Stop'Map{}() : Map{} []
hooked-symbol LblminInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol Lbl'Unds-LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Bool{} []
hooked-symbol Lblkeys{}(Map{}) : Set{} []
symbol LblisKItem{}(K{}) : Bool{} []
hooked-symbol LblSet'Coln'difference{}(Set{}, Set{}) : Set{} []
symbol Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(K{}) : KItem{} []
hooked-symbol LblString2Int{}(String{}) : Int{} []
hooked-symbol Lbl'Unds-LT-Eqls'Set'UndsUnds'SET'UndsUnds'Set'Unds'Set{}(Set{}, Set{}) : Bool{} []
hooked-symbol LbldirectionalityChar{}(String{}) : String{} []
symbol Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K{}) : KItem{} []
hooked-symbol LblsizeList{}(List{}) : Int{} []
symbol LblisKConfigVar{}(K{}) : Bool{} []
symbol Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K{}) : KItem{} []
symbol Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}() : Block{} []
symbol Lbl'-LT-'T'-GT-'-fragment{}(KCellOpt{}, StateCellOpt{}) : TCellFragment{} []
hooked-symbol Lbl'UndsEqlsEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Bool{}, Bool{}) : Bool{} []
symbol LblnoKCell{}() : KCellOpt{} []
hooked-symbol Lbl'Unds'-Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
symbol LblisKCell{}(K{}) : Bool{} []
hooked-symbol LblFloatFormat{}(Float{}, String{}) : String{} []
symbol LblisPgm{}(K{}) : Bool{} []
hooked-symbol LblmaxInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
hooked-symbol LblsubstrString{}(String{}, Int{}, Int{}) : String{} []
symbol Lbl'-LT-'k'-GT-'{}(K{}) : KCell{} []
hooked-symbol LblabsInt{}(Int{}) : Int{} []
hooked-symbol Lbl'Unds'andBool'Unds'{}(Bool{}, Bool{}) : Bool{} []
symbol LblisAExp{}(K{}) : Bool{} []
symbol Lbl'Unds'Set'Unds'{}(Set{}, Set{}) : Set{} []
symbol LblfreshInt{}(Int{}) : Int{} []
symbol Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(BExp{}, Block{}, Block{}) : Stmt{} []
hooked-symbol Lbl'UndsXor-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Int{}, Int{}) : Int{} []
symbol Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(K{}) : KItem{} []
hooked-symbol LblordChar{}(String{}) : Int{} []
hooked-symbol Lbl'UndsEqlsSlshEqls'K'UndsUnds'K-EQUAL'UndsUnds'K'Unds'K{}(K{}, K{}) : Bool{} []
symbol LblisFloat{}(K{}) : Bool{} []
symbol Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(Stmt{}) : Block{} []
symbol LblisBlock{}(K{}) : Bool{} []
hooked-symbol Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'UndsUnds'K'Unds'Map{}(K{}, Map{}) : Bool{} []
// generated axioms
axiom{R} \exists{R} (Val:KCell{}, \equals{KCell{}, R} (Val:KCell{}, LblinitKCell{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, Lbl'Stop'Set{}())) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblInt2String{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, Lblkeys'Unds'list'LParUndsRParUnds'MAP'UndsUnds'Map{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-GT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds'xorInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:BExp{}, \equals{BExp{}, R} (Val:BExp{}, Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(K0:BExp{}))) [] // functional
axiom{}\implies{BExp{}} (\and{BExp{}} (Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(X0:BExp{}), Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(Y0:BExp{})), Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(\and{BExp{}} (X0:BExp{}, Y0:BExp{}))) [] // no confusion same constructor
axiom{}\not{BExp{}} (\and{BExp{}} (Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(X0:BExp{}), Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{}))) [] // no confusion different constructors
axiom{}\not{BExp{}} (\and{BExp{}} (Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(X0:BExp{}), Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(Y0:BExp{}, Y1:BExp{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisKResult{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'dividesInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblchrChar{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblreplaceFirst'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(K0:String{}, K1:String{}, K2:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Pgm{}, \equals{Pgm{}, R} (Val:Pgm{}, Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(K0:Ids{}, K1:Stmt{}))) [] // functional
axiom{}\implies{Pgm{}} (\and{Pgm{}} (Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(X0:Ids{}, X1:Stmt{}), Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(Y0:Ids{}, Y1:Stmt{})), Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(\and{Ids{}} (X0:Ids{}, Y0:Ids{}), \and{Stmt{}} (X1:Stmt{}, Y1:Stmt{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsEqls'K'Unds'{}(K0:K{}, K1:K{}))) [] // functional
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, LblListItem{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisStateCellOpt{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, LblintersectSet{}(K0:Set{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisKCellOpt{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Stmt{}, \equals{Stmt{}, R} (Val:Stmt{}, Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(K0:Id{}, K1:AExp{}))) [] // functional
axiom{}\implies{Stmt{}} (\and{Stmt{}} (Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(X0:Id{}, X1:AExp{}), Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(Y0:Id{}, Y1:AExp{})), Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(\and{Id{}} (X0:Id{}, Y0:Id{}), \and{AExp{}} (X1:AExp{}, Y1:AExp{}))) [] // no confusion same constructor
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(X0:Id{}, X1:AExp{}), Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(Y0:BExp{}, Y1:Block{}))) [] // no confusion different constructors
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(X0:Id{}, X1:AExp{}), Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(Y0:Stmt{}, Y1:Stmt{}))) [] // no confusion different constructors
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(X0:Id{}, X1:AExp{}), Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(Y0:BExp{}, Y1:Block{}, Y2:Block{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisBool{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'UndsLSqBUnds-LT-'-undef'RSqB'{}(K0:Map{}, K1:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsAnd'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, LblremoveAll{}(K0:Map{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:TCell{}, \equals{TCell{}, R} (Val:TCell{}, Lbl'-LT-'T'-GT-'{}(K0:KCell{}, K1:StateCell{}))) [] // functional
axiom{}\implies{TCell{}} (\and{TCell{}} (Lbl'-LT-'T'-GT-'{}(X0:KCell{}, X1:StateCell{}), Lbl'-LT-'T'-GT-'{}(Y0:KCell{}, Y1:StateCell{})), Lbl'-LT-'T'-GT-'{}(\and{KCell{}} (X0:KCell{}, Y0:KCell{}), \and{StateCell{}} (X1:StateCell{}, Y1:StateCell{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisTCell{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblSet'Coln'in{}(K0:K{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblsrandInt{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisIds{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblrandInt{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisStmt{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblMap'Coln'choice{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:BExp{}, \equals{BExp{}, R} (Val:BExp{}, Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(K0:AExp{}, K1:AExp{}))) [] // functional
axiom{}\implies{BExp{}} (\and{BExp{}} (Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}), Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{})), Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(\and{AExp{}} (X0:AExp{}, Y0:AExp{}), \and{AExp{}} (X1:AExp{}, Y1:AExp{}))) [] // no confusion same constructor
axiom{}\not{BExp{}} (\and{BExp{}} (Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}), Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(Y0:BExp{}, Y1:BExp{}))) [] // no confusion different constructors
axiom{R} \equals{Map{}, R} (Lbl'Unds'Map'Unds'{}(Lbl'Unds'Map'Unds'{}(K1:Map{},K2:Map{}),K3:Map{}),Lbl'Unds'Map'Unds'{}(K1:Map{},Lbl'Unds'Map'Unds'{}(K2:Map{},K3:Map{}))) [] // associativity
axiom{R} \equals{Map{}, R} (Lbl'Unds'Map'Unds'{}(K1:Map{},K2:Map{}),Lbl'Unds'Map'Unds'{}(K2:Map{},K1:Map{})) [] // commutativity
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'Unds'Map'Unds'{}(K0:Map{}, K1:Map{}))) [] // functional
axiom{R} \equals{List{}, R} (Lbl'Unds'List'Unds'{}(Lbl'Unds'List'Unds'{}(K1:List{},K2:List{}),K3:List{}),Lbl'Unds'List'Unds'{}(K1:List{},Lbl'Unds'List'Unds'{}(K2:List{},K3:List{}))) [] // associativity
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, Lbl'Unds'List'Unds'{}(K0:List{}, K1:List{}))) [] // functional
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblSet'Coln'choice{}(K0:Set{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisBExp{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds'divInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsXor-Perc'Int'UndsUndsUnds'INT'UndsUnds'Int'Unds'Int'Unds'Int{}(K0:Int{}, K1:Int{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsPerc'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblreplaceAll'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(K0:String{}, K1:String{}, K2:String{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(Y0:K{}, Y1:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsSlshEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:AExp{}, \equals{AExp{}, R} (Val:AExp{}, Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(K0:Int{}))) [] // functional
axiom{}\implies{AExp{}} (\and{AExp{}} (Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(X0:Int{}), Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(Y0:Int{})), Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(\and{Int{}} (X0:Int{}, Y0:Int{}))) [] // no confusion same constructor
axiom{}\not{AExp{}} (\and{AExp{}} (Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(X0:Int{}), Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{}))) [] // no confusion different constructors
axiom{}\not{AExp{}} (\and{AExp{}} (Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(X0:Int{}), Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lblsize{}(K0:Set{}))) [] // functional
axiom{R} \exists{R} (Val:Stmt{}, \equals{Stmt{}, R} (Val:Stmt{}, Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(K0:BExp{}, K1:Block{}))) [] // functional
axiom{}\implies{Stmt{}} (\and{Stmt{}} (Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(X0:BExp{}, X1:Block{}), Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(Y0:BExp{}, Y1:Block{})), Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(\and{BExp{}} (X0:BExp{}, Y0:BExp{}), \and{Block{}} (X1:Block{}, Y1:Block{}))) [] // no confusion same constructor
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(X0:BExp{}, X1:Block{}), Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(Y0:Stmt{}, Y1:Stmt{}))) [] // no confusion different constructors
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(X0:BExp{}, X1:Block{}), Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(Y0:BExp{}, Y1:Block{}, Y2:Block{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:BExp{}, \equals{BExp{}, R} (Val:BExp{}, Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(K0:BExp{}, K1:BExp{}))) [] // functional
axiom{}\implies{BExp{}} (\and{BExp{}} (Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(X0:BExp{}, X1:BExp{}), Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(Y0:BExp{}, Y1:BExp{})), Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(\and{BExp{}} (X0:BExp{}, Y0:BExp{}), \and{BExp{}} (X1:BExp{}, Y1:BExp{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblfindChar{}(K0:String{}, K1:String{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisK{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'inList'Unds'{}(K0:K{}, K1:List{}))) [] // functional
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, Lbl'Stop'List{}())) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(K0:String{}, K1:String{}, K2:String{}, K3:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisMap{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:StateCellOpt{}, \equals{StateCellOpt{}, R} (Val:StateCellOpt{}, LblnoStateCell{}())) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisTCellFragment{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(Y0:K{}, Y1:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Tild'Int'UndsUnds'INT'UndsUnds'Int{}(K0:Int{}))) [] // functional
axiom{R, S0} \exists{R} (Val:S0, \equals{S0, R} (Val:S0, Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{S0}(K0:Bool{}, K1:S0, K2:S0))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-GT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'UndsLSqBUnds-LT-'-'UndsRSqBUnds'MAP'UndsUnds'Map'Unds'K'Unds'K{}(K0:Map{}, K1:K{}, K2:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblString2Base{}(K0:String{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisId{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LbllengthString{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds-LT--LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsSlshEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:TCell{}, \equals{TCell{}, R} (Val:TCell{}, LblinitTCell{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisSet{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsEqls'Int'Unds'{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Id{}, \equals{Id{}, R} (Val:Id{}, LblfreshId{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, LblupdateMap{}(K0:Map{}, K1:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblrfindChar{}(K0:String{}, K1:String{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblMap'Coln'lookup{}(K0:Map{}, K1:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisString{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, Lblvalues{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds'modInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'Unds'-Map'UndsUnds'MAP'UndsUnds'Map'Unds'Map{}(K0:Map{}, K1:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisInt{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblfindString{}(K0:String{}, K1:String{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Ids{}, \equals{Ids{}, R} (Val:Ids{}, Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(K0:Id{}, K1:Ids{}))) [] // functional
axiom{}\implies{Ids{}} (\and{Ids{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(X0:Id{}, X1:Ids{}), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(Y0:Id{}, Y1:Ids{})), Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(\and{Id{}} (X0:Id{}, Y0:Id{}), \and{Ids{}} (X1:Ids{}, Y1:Ids{}))) [] // no confusion same constructor
axiom{}\not{Ids{}} (\and{Ids{}} (Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(X0:Id{}, X1:Ids{}), Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'UndsQuotRBraUnds'Ids{}())) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Float{}, \equals{Float{}, R} (Val:Float{}, LblString2Float{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsPipe'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisCell{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:Id{}, \equals{Id{}, R} (Val:Id{}, LblString2Id{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(K0:K{}, K1:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(Y0:K{}, Y1:K{})), Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}), \and{K{}} (X1:K{}, Y1:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblList'Coln'get{}(K0:List{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:AExp{}, \equals{AExp{}, R} (Val:AExp{}, Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(K0:AExp{}, K1:AExp{}))) [] // functional
axiom{}\implies{AExp{}} (\and{AExp{}} (Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}), Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{})), Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(\and{AExp{}} (X0:AExp{}, Y0:AExp{}), \and{AExp{}} (X1:AExp{}, Y1:AExp{}))) [] // no confusion same constructor
axiom{}\not{AExp{}} (\and{AExp{}} (Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}), Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblsizeMap{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblId2String{}(K0:Id{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{})), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblnotBool'Unds'{}(K0:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:List{}, \equals{List{}, R} (Val:List{}, LblList'Coln'range{}(K0:List{}, K1:Int{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:AExp{}, \equals{AExp{}, R} (Val:AExp{}, Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(K0:AExp{}, K1:AExp{}))) [] // functional
axiom{}\implies{AExp{}} (\and{AExp{}} (Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}), Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(Y0:AExp{}, Y1:AExp{})), Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(\and{AExp{}} (X0:AExp{}, Y0:AExp{}), \and{AExp{}} (X1:AExp{}, Y1:AExp{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Ids{}, \equals{Ids{}, R} (Val:Ids{}, Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'UndsQuotRBraUnds'Ids{}())) [] // functional
axiom{R} \exists{R} (Val:Stmt{}, \equals{Stmt{}, R} (Val:Stmt{}, Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(K0:Stmt{}, K1:Stmt{}))) [] // functional
axiom{}\implies{Stmt{}} (\and{Stmt{}} (Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(X0:Stmt{}, X1:Stmt{}), Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(Y0:Stmt{}, Y1:Stmt{})), Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(\and{Stmt{}} (X0:Stmt{}, Y0:Stmt{}), \and{Stmt{}} (X1:Stmt{}, Y1:Stmt{}))) [] // no confusion same constructor
axiom{}\not{Stmt{}} (\and{Stmt{}} (Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(X0:Stmt{}, X1:Stmt{}), Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(Y0:BExp{}, Y1:Block{}, Y2:Block{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{})), Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-Eqls'Map'UndsUnds'MAP'UndsUnds'Map'Unds'Map{}(K0:Map{}, K1:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblrfindString{}(K0:String{}, K1:String{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:StateCell{}, \equals{StateCell{}, R} (Val:StateCell{}, Lbl'-LT-'state'-GT-'{}(K0:Map{}))) [] // functional
axiom{}\implies{StateCell{}} (\and{StateCell{}} (Lbl'-LT-'state'-GT-'{}(X0:Map{}), Lbl'-LT-'state'-GT-'{}(Y0:Map{})), Lbl'-LT-'state'-GT-'{}(\and{Map{}} (X0:Map{}, Y0:Map{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblFloat2String{}(K0:Float{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-GT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(K0:String{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisStateCell{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}())) [] // functional
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds-GT--GT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'UndsPipe'-'-GT-Unds'{}(K0:K{}, K1:K{}))) [] // functional
axiom{R} \exists{R} (Val:K{}, \equals{K{}, R} (Val:K{}, LblMap'Coln'lookupOrDefault{}(K0:Map{}, K1:K{}, K2:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisList{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsStar'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-GT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblcategoryChar{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsSlsh'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblBase2String{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, LblSetItem{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:StateCell{}, \equals{StateCell{}, R} (Val:StateCell{}, LblinitStateCell{}())) [] // functional
axiom{R} \exists{R} (Val:Map{}, \equals{Map{}, R} (Val:Map{}, Lbl'Stop'Map{}())) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblminInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, Lblkeys{}(K0:Map{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisKItem{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, LblSet'Coln'difference{}(K0:Set{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblString2Int{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds-LT-Eqls'Set'UndsUnds'SET'UndsUnds'Set'Unds'Set{}(K0:Set{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LbldirectionalityChar{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblsizeList{}(K0:List{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisKConfigVar{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{}\not{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:Block{}, \equals{Block{}, R} (Val:Block{}, Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}())) [] // functional
axiom{}\not{Block{}} (\and{Block{}} (Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}(), Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(Y0:Stmt{}))) [] // no confusion different constructors
axiom{R} \exists{R} (Val:TCellFragment{}, \equals{TCellFragment{}, R} (Val:TCellFragment{}, Lbl'-LT-'T'-GT-'-fragment{}(K0:KCellOpt{}, K1:StateCellOpt{}))) [] // functional
axiom{}\implies{TCellFragment{}} (\and{TCellFragment{}} (Lbl'-LT-'T'-GT-'-fragment{}(X0:KCellOpt{}, X1:StateCellOpt{}), Lbl'-LT-'T'-GT-'-fragment{}(Y0:KCellOpt{}, Y1:StateCellOpt{})), Lbl'-LT-'T'-GT-'-fragment{}(\and{KCellOpt{}} (X0:KCellOpt{}, Y0:KCellOpt{}), \and{StateCellOpt{}} (X1:StateCellOpt{}, Y1:StateCellOpt{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:KCellOpt{}, \equals{KCellOpt{}, R} (Val:KCellOpt{}, LblnoKCell{}())) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'Unds'-Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisKCell{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblFloatFormat{}(K0:Float{}, K1:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisPgm{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblmaxInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:String{}, \equals{String{}, R} (Val:String{}, LblsubstrString{}(K0:String{}, K1:Int{}, K2:Int{}))) [] // functional
axiom{R} \exists{R} (Val:KCell{}, \equals{KCell{}, R} (Val:KCell{}, Lbl'-LT-'k'-GT-'{}(K0:K{}))) [] // functional
axiom{}\implies{KCell{}} (\and{KCell{}} (Lbl'-LT-'k'-GT-'{}(X0:K{}), Lbl'-LT-'k'-GT-'{}(Y0:K{})), Lbl'-LT-'k'-GT-'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblabsInt{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'andBool'Unds'{}(K0:Bool{}, K1:Bool{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisAExp{}(K0:K{}))) [] // functional
axiom{R} \equals{Set{}, R} (Lbl'Unds'Set'Unds'{}(Lbl'Unds'Set'Unds'{}(K1:Set{},K2:Set{}),K3:Set{}),Lbl'Unds'Set'Unds'{}(K1:Set{},Lbl'Unds'Set'Unds'{}(K2:Set{},K3:Set{}))) [] // associativity
axiom{R} \equals{Set{}, R} (Lbl'Unds'Set'Unds'{}(K1:Set{},K2:Set{}),Lbl'Unds'Set'Unds'{}(K2:Set{},K1:Set{})) [] // commutativity
axiom{R} \equals{Set{}, R} (Lbl'Unds'Set'Unds'{}(K:Set{},K:Set{}),K:Set{}) [] // idempotency
axiom{R} \exists{R} (Val:Set{}, \equals{Set{}, R} (Val:Set{}, Lbl'Unds'Set'Unds'{}(K0:Set{}, K1:Set{}))) [] // functional
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblfreshInt{}(K0:Int{}))) [] // functional
axiom{R} \exists{R} (Val:Stmt{}, \equals{Stmt{}, R} (Val:Stmt{}, Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(K0:BExp{}, K1:Block{}, K2:Block{}))) [] // functional
axiom{}\implies{Stmt{}} (\and{Stmt{}} (Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(X0:BExp{}, X1:Block{}, X2:Block{}), Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(Y0:BExp{}, Y1:Block{}, Y2:Block{})), Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(\and{BExp{}} (X0:BExp{}, Y0:BExp{}), \and{Block{}} (X1:Block{}, Y1:Block{}), \and{Block{}} (X2:Block{}, Y2:Block{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, Lbl'UndsXor-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(K0:Int{}, K1:Int{}))) [] // functional
axiom{R} \exists{R} (Val:KItem{}, \equals{KItem{}, R} (Val:KItem{}, Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(K0:K{}))) [] // functional
axiom{}\implies{KItem{}} (\and{KItem{}} (Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(X0:K{}), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(Y0:K{})), Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(\and{K{}} (X0:K{}, Y0:K{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Int{}, \equals{Int{}, R} (Val:Int{}, LblordChar{}(K0:String{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'UndsEqlsSlshEqls'K'UndsUnds'K-EQUAL'UndsUnds'K'Unds'K{}(K0:K{}, K1:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisFloat{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Block{}, \equals{Block{}, R} (Val:Block{}, Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(K0:Stmt{}))) [] // functional
axiom{}\implies{Block{}} (\and{Block{}} (Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(X0:Stmt{}), Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(Y0:Stmt{})), Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(\and{Stmt{}} (X0:Stmt{}, Y0:Stmt{}))) [] // no confusion same constructor
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, LblisBlock{}(K0:K{}))) [] // functional
axiom{R} \exists{R} (Val:Bool{}, \equals{Bool{}, R} (Val:Bool{}, Lbl'Unds'in'Unds'keys'LParUndsRParUnds'MAP'UndsUnds'K'Unds'Map{}(K0:K{}, K1:Map{}))) [] // functional
axiom{} \or{KItem{}} (\exists{KItem{}} (Val:Int{}, inj{Int{}, KItem{}} (Val:Int{})), \or{KItem{}} (\exists{KItem{}} (Val:Pgm{}, inj{Pgm{}, KItem{}} (Val:Pgm{})), \or{KItem{}} (\exists{KItem{}} (Val:KCell{}, inj{KCell{}, KItem{}} (Val:KCell{})), \or{KItem{}} (\exists{KItem{}} (Val:StateCellOpt{}, inj{StateCellOpt{}, KItem{}} (Val:StateCellOpt{})), \or{KItem{}} (\exists{KItem{}} (Val:Set{}, inj{Set{}, KItem{}} (Val:Set{})), \or{KItem{}} (\exists{KItem{}} (Val:AExp{}, inj{AExp{}, KItem{}} (Val:AExp{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (Val:Map{}, inj{Map{}, KItem{}} (Val:Map{})), \or{KItem{}} (\exists{KItem{}} (Val:TCell{}, inj{TCell{}, KItem{}} (Val:TCell{})), \or{KItem{}} (\exists{KItem{}} (Val:List{}, inj{List{}, KItem{}} (Val:List{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (Val:TCellFragment{}, inj{TCellFragment{}, KItem{}} (Val:TCellFragment{})), \or{KItem{}} (\exists{KItem{}} (Val:StateCell{}, inj{StateCell{}, KItem{}} (Val:StateCell{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, \exists{KItem{}} (X1:K{}, Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(X0:K{}, X1:K{}))), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (Val:Cell{}, inj{Cell{}, KItem{}} (Val:Cell{})), \or{KItem{}} (\exists{KItem{}} (Val:Bool{}, inj{Bool{}, KItem{}} (Val:Bool{})), \or{KItem{}} (\exists{KItem{}} (Val:Float{}, inj{Float{}, KItem{}} (Val:Float{})), \or{KItem{}} (Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(), \or{KItem{}} (\exists{KItem{}} (Val:Ids{}, inj{Ids{}, KItem{}} (Val:Ids{})), \or{KItem{}} (\exists{KItem{}} (Val:Id{}, inj{Id{}, KItem{}} (Val:Id{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (Val:Stmt{}, inj{Stmt{}, KItem{}} (Val:Stmt{})), \or{KItem{}} (\exists{KItem{}} (Val:BExp{}, inj{BExp{}, KItem{}} (Val:BExp{})), \or{KItem{}} (\exists{KItem{}} (Val:KCellOpt{}, inj{KCellOpt{}, KItem{}} (Val:KCellOpt{})), \or{KItem{}} (\exists{KItem{}} (X0:K{}, Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(X0:K{})), \or{KItem{}} (\exists{KItem{}} (Val:String{}, inj{String{}, KItem{}} (Val:String{})), \or{KItem{}} (\exists{KItem{}} (Val:KResult{}, inj{KResult{}, KItem{}} (Val:KResult{})), \or{KItem{}} (\exists{KItem{}} (Val:Block{}, inj{Block{}, KItem{}} (Val:Block{})), \bottom{KItem{}}())))))))))))))))))))))))))))))))) [] // no junk
axiom{} \or{List{}} (\exists{List{}} (X0:List{}, \exists{List{}} (X1:List{}, Lbl'Unds'List'Unds'{}(X0:List{}, X1:List{}))), \or{List{}} (Lbl'Stop'List{}(), \bottom{List{}}())) [] // no junk
axiom{} \or{TCellFragment{}} (\exists{TCellFragment{}} (X0:KCellOpt{}, \exists{TCellFragment{}} (X1:StateCellOpt{}, Lbl'-LT-'T'-GT-'-fragment{}(X0:KCellOpt{}, X1:StateCellOpt{}))), \bottom{TCellFragment{}}()) [] // no junk
axiom{} \or{String{}} (\top{String{}}(), \bottom{String{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{StateCell{}} (\exists{StateCell{}} (X0:Map{}, Lbl'-LT-'state'-GT-'{}(X0:Map{})), \bottom{StateCell{}}()) [] // no junk
axiom{} \or{KConfigVar{}} (\top{KConfigVar{}}(), \bottom{KConfigVar{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{TCell{}} (\exists{TCell{}} (X0:KCell{}, \exists{TCell{}} (X1:StateCell{}, Lbl'-LT-'T'-GT-'{}(X0:KCell{}, X1:StateCell{}))), \bottom{TCell{}}()) [] // no junk
axiom{} \or{Ids{}} (\exists{Ids{}} (X0:Id{}, \exists{Ids{}} (X1:Ids{}, Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(X0:Id{}, X1:Ids{}))), \or{Ids{}} (Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'UndsQuotRBraUnds'Ids{}(), \bottom{Ids{}}())) [] // no junk
axiom{} \or{BExp{}} (\exists{BExp{}} (X0:BExp{}, Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(X0:BExp{})), \or{BExp{}} (\exists{BExp{}} (X0:AExp{}, \exists{BExp{}} (X1:AExp{}, Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}))), \or{BExp{}} (\exists{BExp{}} (X0:BExp{}, \exists{BExp{}} (X1:BExp{}, Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(X0:BExp{}, X1:BExp{}))), \or{BExp{}} (\exists{BExp{}} (Val:Bool{}, inj{Bool{}, BExp{}} (Val:Bool{})), \bottom{BExp{}}())))) [] // no junk
axiom{} \or{StateCellOpt{}} (LblnoStateCell{}(), \or{StateCellOpt{}} (\exists{StateCellOpt{}} (Val:StateCell{}, inj{StateCell{}, StateCellOpt{}} (Val:StateCell{})), \bottom{StateCellOpt{}}())) [] // no junk
axiom{} \or{Id{}} (\top{Id{}}(), \bottom{Id{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{Cell{}} (\exists{Cell{}} (Val:KCell{}, inj{KCell{}, Cell{}} (Val:KCell{})), \or{Cell{}} (\exists{Cell{}} (Val:TCell{}, inj{TCell{}, Cell{}} (Val:TCell{})), \or{Cell{}} (\exists{Cell{}} (Val:StateCell{}, inj{StateCell{}, Cell{}} (Val:StateCell{})), \bottom{Cell{}}()))) [] // no junk
axiom{} \or{Bool{}} (\top{Bool{}}(), \bottom{Bool{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{KCell{}} (\exists{KCell{}} (X0:K{}, Lbl'-LT-'k'-GT-'{}(X0:K{})), \bottom{KCell{}}()) [] // no junk
axiom{} \or{K{}} (\exists{K{}} (Val:KItem{}, inj{KItem{}, K{}} (Val:KItem{})), \bottom{K{}}()) [] // no junk
axiom{} \or{KResult{}} (\exists{KResult{}} (Val:Int{}, inj{Int{}, KResult{}} (Val:Int{})), \or{KResult{}} (\exists{KResult{}} (Val:Bool{}, inj{Bool{}, KResult{}} (Val:Bool{})), \bottom{KResult{}}())) [] // no junk
axiom{} \or{Map{}} (\exists{Map{}} (X0:Map{}, \exists{Map{}} (X1:Map{}, Lbl'Unds'Map'Unds'{}(X0:Map{}, X1:Map{}))), \or{Map{}} (Lbl'Stop'Map{}(), \bottom{Map{}}())) [] // no junk
axiom{} \or{KCellOpt{}} (\exists{KCellOpt{}} (Val:KCell{}, inj{KCell{}, KCellOpt{}} (Val:KCell{})), \or{KCellOpt{}} (LblnoKCell{}(), \bottom{KCellOpt{}}())) [] // no junk
axiom{} \or{Stmt{}} (\exists{Stmt{}} (X0:Id{}, \exists{Stmt{}} (X1:AExp{}, Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(X0:Id{}, X1:AExp{}))), \or{Stmt{}} (\exists{Stmt{}} (Val:Block{}, inj{Block{}, Stmt{}} (Val:Block{})), \or{Stmt{}} (\exists{Stmt{}} (X0:BExp{}, \exists{Stmt{}} (X1:Block{}, Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(X0:BExp{}, X1:Block{}))), \or{Stmt{}} (\exists{Stmt{}} (X0:Stmt{}, \exists{Stmt{}} (X1:Stmt{}, Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(X0:Stmt{}, X1:Stmt{}))), \or{Stmt{}} (\exists{Stmt{}} (X0:BExp{}, \exists{Stmt{}} (X1:Block{}, \exists{Stmt{}} (X2:Block{}, Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(X0:BExp{}, X1:Block{}, X2:Block{})))), \bottom{Stmt{}}()))))) [] // no junk
axiom{} \or{Int{}} (\top{Int{}}(), \bottom{Int{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{Float{}} (\top{Float{}}(), \bottom{Float{}}()) [] // no junk (TODO: fix bug with \dv)
axiom{} \or{Pgm{}} (\exists{Pgm{}} (X0:Ids{}, \exists{Pgm{}} (X1:Stmt{}, Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(X0:Ids{}, X1:Stmt{}))), \bottom{Pgm{}}()) [] // no junk
axiom{} \or{Block{}} (Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}(), \or{Block{}} (\exists{Block{}} (X0:Stmt{}, Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(X0:Stmt{})), \bottom{Block{}}())) [] // no junk
axiom{} \or{Set{}} (Lbl'Stop'Set{}(), \or{Set{}} (\exists{Set{}} (X0:Set{}, \exists{Set{}} (X1:Set{}, Lbl'Unds'Set'Unds'{}(X0:Set{}, X1:Set{}))), \bottom{Set{}}())) [] // no junk
axiom{} \or{AExp{}} (\exists{AExp{}} (Val:Id{}, inj{Id{}, AExp{}} (Val:Id{})), \or{AExp{}} (\exists{AExp{}} (Val:Int{}, inj{Int{}, AExp{}} (Val:Int{})), \or{AExp{}} (\exists{AExp{}} (X0:Int{}, Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(X0:Int{})), \or{AExp{}} (\exists{AExp{}} (X0:AExp{}, \exists{AExp{}} (X1:AExp{}, Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}))), \or{AExp{}} (\exists{AExp{}} (X0:AExp{}, \exists{AExp{}} (X1:AExp{}, Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(X0:AExp{}, X1:AExp{}))), \bottom{AExp{}}()))))) [] // no junk
// rules
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_/__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(`_/__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() left() org.kframework.attributes.Location(Location(32,20,32,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1712977715) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isIds(inj{Ids,K}(Ids))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisIds{}(inj{Ids{}, K{}}(VarIds:Ids{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_+__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_+__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() left() org.kframework.attributes.Location(Location(33,20,33,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(329733001) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule isKItem(inj{KItem,K}(KItem))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{KItem{}, K{}}(VarKItem:KItem{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isBExp(inj{BExp,K}(BExp))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisBExp{}(inj{BExp{}, K{}}(VarBExp:BExp{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isMap(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarMap:Map{},
\and{Bool{}} (
\top{Bool{}}(),
LblisMap{}(inj{Map{}, K{}}(VarMap:Map{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisMap{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_/__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_/__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() left() org.kframework.attributes.Location(Location(32,20,32,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1712977715) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `minInt(_,_)_INT__Int_Int`(I1,I2)=>I1 requires `_<=Int__INT__Int_Int`(I1,I2) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(371) org.kframework.attributes.Location(Location(371,8,371,57)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-LT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblminInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
VarI1:Int{}),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_<=__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(`_<=__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() latex({#1}\leq{#2}) org.kframework.attributes.Location(Location(36,20,36,91)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(242352470) seqstrict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isKCell(inj{KCell,K}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKCell{}(inj{KCell{}, K{}}(VarKCell:KCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_+__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(`_+__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() left() org.kframework.attributes.Location(Location(33,20,33,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(329733001) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isKItem(inj{Ids,K}(Ids))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Ids{}, K{}}(VarIds:Ids{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isList(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarList:List{},
\and{Bool{}} (
\top{Bool{}}(),
LblisList{}(inj{List{}, K{}}(VarList:List{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisList{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isFloat(inj{Float,K}(Float))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisFloat{}(inj{Float{}, K{}}(VarFloat:Float{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_&&__IMP-SYNTAX__BExp_BExp`(HOLE,K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezer_&&__IMP-SYNTAX__BExp_BExp1_`(inj{BExp,K}(K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() left() org.kframework.attributes.Location(Location(38,20,38,76)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1616548737) strict(1)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(VarHOLE:BExp{},VarK1:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(inj{BExp{}, K{}}(VarK1:BExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule isAExp(inj{Int,K}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisAExp{}(inj{Int{}, K{}}(VarInt:Int{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isIds(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarIds:Ids{},
\and{Bool{}} (
\top{Bool{}}(),
LblisIds{}(inj{Ids{}, K{}}(VarIds:Ids{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisIds{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule findChar(S1,S2,I)=>`#if_#then_#else_#fi_K-EQUAL__Bool_K_K`(`_==Int_`(findString(S1,substrString(S2,#token("0","Int"),#token("1","Int")),I),#token("-1","Int")),findChar(S1,substrString(S2,#token("1","Int"),lengthString(S2)),I),`#if_#then_#else_#fi_K-EQUAL__Bool_K_K`(`_==Int_`(findChar(S1,substrString(S2,#token("1","Int"),lengthString(S2)),I),#token("-1","Int")),findString(S1,substrString(S2,#token("0","Int"),#token("1","Int")),I),`minInt(_,_)_INT__Int_Int`(findString(S1,substrString(S2,#token("0","Int"),#token("1","Int")),I),findChar(S1,substrString(S2,#token("1","Int"),lengthString(S2)),I)))) requires `_=/=String__STRING__String_String`(S2,#token("\"\"","String")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(532) org.kframework.attributes.Location(Location(532,8,532,431)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'UndsEqlsSlshEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS2:String{},\dv{String{}}("\"\"")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblfindChar{}(VarS1:String{},VarS2:String{},VarI:Int{}),
Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{Int{}}(Lbl'UndsEqlsEqls'Int'Unds'{}(LblfindString{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("0"),\dv{Int{}}("1")),VarI:Int{}),\dv{Int{}}("-1")),LblfindChar{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("1"),LbllengthString{}(VarS2:String{})),VarI:Int{}),Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{Int{}}(Lbl'UndsEqlsEqls'Int'Unds'{}(LblfindChar{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("1"),LbllengthString{}(VarS2:String{})),VarI:Int{}),\dv{Int{}}("-1")),LblfindString{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("0"),\dv{Int{}}("1")),VarI:Int{}),LblminInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("0"),\dv{Int{}}("1")),VarI:Int{}),LblfindChar{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("1"),LbllengthString{}(VarS2:String{})),VarI:Int{}))))),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezerif(_)_else__IMP-SYNTAX__BExp_Block_Block1_`(inj{Block,K}(K1),inj{Block,K}(K2))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(`if(_)_else__IMP-SYNTAX__BExp_Block_Block`(HOLE,K1,K2))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [colors(yellow, white, white, yellow) cool() format(%1 %2%3%4 %5 %6 %7) org.kframework.attributes.Location(Location(44,20,45,123)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1027937315) strict(1)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(inj{Block{}, K{}}(VarK1:Block{}),inj{Block{}, K{}}(VarK2:Block{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(VarHOLE:BExp{},VarK1:Block{},VarK2:Block{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isKItem(inj{KCellOpt,K}(KCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{KCellOpt{}, K{}}(VarKCellOpt:KCellOpt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `replaceAll(_,_,_)_STRING__String_String_String`(Source,ToReplace,Replacement)=>`replace(_,_,_,_)_STRING__String_String_String_Int`(Source,ToReplace,Replacement,`countAllOccurrences(_,_)_STRING__String_String`(Source,ToReplace)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(554) org.kframework.attributes.Location(Location(554,8,554,154)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{String{},R} (
LblreplaceAll'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(VarSource:String{},VarToReplace:String{},VarReplacement:String{}),
Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(VarSource:String{},VarToReplace:String{},VarReplacement:String{},LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(VarSource:String{},VarToReplace:String{}))),
\top{R}()))
[]
// rule `_andBool_`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(285) org.kframework.attributes.Location(Location(285,8,285,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andBool'Unds'{}(\dv{Bool{}}("true"),VarB:Bool{}),
VarB:Bool{}),
\top{R}()))
[]
// rule isTCell(inj{TCell,K}(TCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisTCell{}(inj{TCell{}, K{}}(VarTCell:TCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{List,K}(List))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{List{}, K{}}(VarList:List{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_xorBool__BOOL__Bool_Bool`(B,B)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(297) org.kframework.attributes.Location(Location(297,8,297,38)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB:Bool{},VarB:Bool{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isSet(inj{Set,K}(Set))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisSet{}(inj{Set{}, K{}}(VarSet:Set{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{KCell,K}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{KCell{}, K{}}(VarKCell:KCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isAExp(inj{AExp,K}(AExp))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisAExp{}(inj{AExp{}, K{}}(VarAExp:AExp{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_orBool__BOOL__Bool_Bool`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(302) org.kframework.attributes.Location(Location(302,8,302,32)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("false"),VarB:Bool{}),
VarB:Bool{}),
\top{R}()))
[]
// rule rfindChar(S1,S2,I)=>`maxInt(_,_)_INT__Int_Int`(rfindString(S1,substrString(S2,#token("0","Int"),#token("1","Int")),I),rfindChar(S1,substrString(S2,#token("1","Int"),lengthString(S2)),I)) requires `_=/=String__STRING__String_String`(S2,#token("\"\"","String")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(534) org.kframework.attributes.Location(Location(534,8,534,182)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'UndsEqlsSlshEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS2:String{},\dv{String{}}("\"\"")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblrfindChar{}(VarS1:String{},VarS2:String{},VarI:Int{}),
LblmaxInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(LblrfindString{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("0"),\dv{Int{}}("1")),VarI:Int{}),LblrfindChar{}(VarS1:String{},LblsubstrString{}(VarS2:String{},\dv{Int{}}("1"),LbllengthString{}(VarS2:String{})),VarI:Int{}))),
\top{R}()))
[]
// rule isCell(inj{StateCell,K}(StateCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisCell{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_+__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_+__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() left() org.kframework.attributes.Location(Location(33,20,33,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(329733001) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `_dividesInt__INT__Int_Int`(I1,I2)=>`_==Int_`(`_%Int__INT__Int_Int`(I2,I1),#token("0","Int")) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(384) org.kframework.attributes.Location(Location(384,8,384,58)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'dividesInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
Lbl'UndsEqlsEqls'Int'Unds'{}(Lbl'UndsPerc'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI2:Int{},VarI1:Int{}),\dv{Int{}}("0"))),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_/__IMP-SYNTAX__AExp_AExp`(inj{Int,AExp}(I1),inj{Int,AExp}(I2)))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Int,KItem}(`_/Int__INT__Int_Int`(I1,I2))~>DotVar1),DotVar0) requires `_=/=Int__INT__Int_Int`(I2,#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(121) org.kframework.attributes.Location(Location(121,8,121,51)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{} \and{TCell{}} (
\equals{Bool{},TCell{}}(
Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI2:Int{},\dv{Int{}}("0")),
\dv{Bool{}}("true")), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(inj{Int{}, AExp{}}(VarI1:Int{}),inj{Int{}, AExp{}}(VarI2:Int{}))),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Int{}, KItem{}}(Lbl'UndsSlsh'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_orElseBool__BOOL__Bool_Bool`(_6,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(306) org.kframework.attributes.Location(Location(306,8,306,33)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Var'Unds'6:Bool{},\dv{Bool{}}("true")),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_impliesBool__BOOL__Bool_Bool`(B,#token("false","Bool"))=>`notBool_`(B) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(313) org.kframework.attributes.Location(Location(313,8,313,45)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB:Bool{},\dv{Bool{}}("false")),
LblnotBool'Unds'{}(VarB:Bool{})),
\top{R}()))
[]
// rule isKItem(inj{Id,K}(Id))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Id{}, K{}}(VarId:Id{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isFloat(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarFloat:Float{},
\and{Bool{}} (
\top{Bool{}}(),
LblisFloat{}(inj{Float{}, K{}}(VarFloat:Float{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisFloat{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isKConfigVar(inj{KConfigVar,K}(KConfigVar))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKConfigVar{}(inj{KConfigVar{}, K{}}(VarKConfigVar:KConfigVar{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{KResult,K}(KResult))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{KResult{}, K{}}(VarKResult:KResult{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isK(K)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisK{}(VarK:K{}),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_xorBool__BOOL__Bool_Bool`(B1,B2)=>`notBool_`(`_==Bool__BOOL__Bool_Bool`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(298) org.kframework.attributes.Location(Location(298,8,298,57)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB1:Bool{},VarB2:Bool{}),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB1:Bool{},VarB2:Bool{}))),
\top{R}()))
[]
// rule `_andBool_`(B,#token("true","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(286) org.kframework.attributes.Location(Location(286,8,286,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andBool'Unds'{}(VarB:Bool{},\dv{Bool{}}("true")),
VarB:Bool{}),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`if(_)_else__IMP-SYNTAX__BExp_Block_Block`(inj{Bool,BExp}(#token("true","Bool")),S,_23))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Block,KItem}(S)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(182) org.kframework.attributes.Location(Location(182,8,182,32)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(inj{Bool{}, BExp{}}(\dv{Bool{}}("true")),VarS:Block{},Var'Unds'23:Block{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Block{}, KItem{}}(VarS:Block{}),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `countAllOccurrences(_,_)_STRING__String_String`(Source,ToCount)=>#token("0","Int") requires `_<Int__INT__Int_Int`(findString(Source,ToCount,#token("0","Int")),#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(537) org.kframework.attributes.Location(Location(537,8,538,59)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToCount:String{},\dv{Int{}}("0")),\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(VarSource:String{},VarToCount:String{}),
\dv{Int{}}("0")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_+__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(`_+__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() left() org.kframework.attributes.Location(Location(33,20,33,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(329733001) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isBExp(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBExp:BExp{},
\and{Bool{}} (
\top{Bool{}}(),
LblisBExp{}(inj{BExp{}, K{}}(VarBExp:BExp{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBool:Bool{},
\and{Bool{}} (
\top{Bool{}}(),
LblisBExp{}(inj{Bool{}, K{}}(VarBool:Bool{}))))),
\bottom{R}()))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisBExp{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_<=__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_<=__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() latex({#1}\leq{#2}) org.kframework.attributes.Location(Location(36,20,36,91)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(242352470) seqstrict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_/__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(`_/__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() left() org.kframework.attributes.Location(Location(32,20,32,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1712977715) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isKResult(inj{Bool,K}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKResult{}(inj{Bool{}, K{}}(VarBool:Bool{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Pgm,K}(`int_;__IMP-SYNTAX__Ids_Stmt`(`_,__IMP-SYNTAX_`(X,Xs),_19))),`<state>`(`_Map_`(Rho,`.Map`(.KList))))=>`<T>`(`<k>`(inj{Pgm,K}(`int_;__IMP-SYNTAX__Ids_Stmt`(Xs,_19))),`<state>`(`_Map_`(Rho,`_|->_`(inj{Id,K}(X),inj{Int,K}(#token("0","Int")))))) requires `notBool_`(`Set:in`(inj{Id,K}(X),keys(Rho))) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(204) org.kframework.attributes.Location(Location(204,8,205,38)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{} \and{TCell{}} (
\equals{Bool{},TCell{}}(
LblnotBool'Unds'{}(LblSet'Coln'in{}(inj{Id{}, K{}}(VarX:Id{}),Lblkeys{}(VarRho:Map{}))),
\dv{Bool{}}("true")), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(inj{Pgm{}, K{}}(Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(Lbl'UndsCommUndsUnds'IMP-SYNTAX'Unds'{}(VarX:Id{},VarXs:Ids{}),Var'Unds'19:Stmt{}))),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(VarRho:Map{},Lbl'Stop'Map{}()))),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(inj{Pgm{}, K{}}(Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(VarXs:Ids{},Var'Unds'19:Stmt{}))),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(VarRho:Map{},Lbl'UndsPipe'-'-GT-Unds'{}(inj{Id{}, K{}}(VarX:Id{}),inj{Int{}, K{}}(\dv{Int{}}("0")))))))))
[]
// rule `notBool_`(#token("false","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(283) org.kframework.attributes.Location(Location(283,8,283,29)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblnotBool'Unds'{}(\dv{Bool{}}("false")),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isSet(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarSet:Set{},
\and{Bool{}} (
\top{Bool{}}(),
LblisSet{}(inj{Set{}, K{}}(VarSet:Set{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisSet{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_>=String__STRING__String_String`(S1,S2)=>`notBool_`(`_<String__STRING__String_String`(S1,S2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(530) org.kframework.attributes.Location(Location(530,8,530,63)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds-GT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}),
LblnotBool'Unds'{}(Lbl'Unds-LT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}))),
\top{R}()))
[]
// rule isStateCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCell:StateCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisStateCellOpt{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCellOpt:StateCellOpt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisStateCellOpt{}(inj{StateCellOpt{}, K{}}(VarStateCellOpt:StateCellOpt{}))))),
\bottom{R}()))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisStateCellOpt{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `#if_#then_#else_#fi_K-EQUAL__Bool_K_K`(C,_11,B2)=>B2 requires `notBool_`(C) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(633) org.kframework.attributes.Location(Location(633,8,633,64)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
LblnotBool'Unds'{}(VarC:Bool{}),
\dv{Bool{}}("true")),
\and{R} (
\equals{K{},R} (
Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{K{}}(VarC:Bool{},Var'Unds'11:K{},VarB2:K{}),
VarB2:K{}),
\top{R}()))
[]
// rule `_impliesBool__BOOL__Bool_Bool`(_3,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(312) org.kframework.attributes.Location(Location(312,8,312,39)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Var'Unds'3:Bool{},\dv{Bool{}}("true")),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`_=_;_IMP-SYNTAX__Id_AExp`(K0,HOLE))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_=_;_IMP-SYNTAX__Id_AExp0_`(inj{Id,K}(K0))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) format(%1 %2 %3%4) heat() org.kframework.attributes.Location(Location(43,20,43,90)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1983769324) strict(2)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(VarK0:Id{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(inj{Id{}, K{}}(VarK0:Id{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule isStateCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCell:StateCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisStateCell{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisStateCell{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_/__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_/__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() left() org.kframework.attributes.Location(Location(32,20,32,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1712977715) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsSlshUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `_=/=Int__INT__Int_Int`(I1,I2)=>`notBool_`(`_==Int_`(I1,I2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(383) org.kframework.attributes.Location(Location(383,8,383,53)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Int'Unds'{}(VarI1:Int{},VarI2:Int{}))),
\top{R}()))
[]
// rule isKItem(inj{BExp,K}(BExp))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{BExp{}, K{}}(VarBExp:BExp{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isBlock(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBlock:Block{},
\and{Bool{}} (
\top{Bool{}}(),
LblisBlock{}(inj{Block{}, K{}}(VarBlock:Block{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisBlock{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `notBool_`(#token("true","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(282) org.kframework.attributes.Location(Location(282,8,282,29)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblnotBool'Unds'{}(\dv{Bool{}}("true")),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `replace(_,_,_,_)_STRING__String_String_String_Int`(Source,_14,_15,#token("0","Int"))=>Source requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(553) org.kframework.attributes.Location(Location(553,8,553,49)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{String{},R} (
Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(VarSource:String{},Var'Unds'14:String{},Var'Unds'15:String{},\dv{Int{}}("0")),
VarSource:String{}),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Id,KItem}(X)~>DotVar1),`<state>`(`_Map_`(`_|->_`(inj{Id,K}(X),I),DotVar2)))=>`<T>`(`<k>`(I~>DotVar1),`<state>`(`_Map_`(`_|->_`(inj{Id,K}(X),I),DotVar2))) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(114) org.kframework.attributes.Location(Location(114,8,114,60)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Id{}, KItem{}}(VarX:Id{}),VarDotVar1:K{})),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{Id{}, K{}}(VarX:Id{}),VarI:K{}),VarDotVar2:Map{}))),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(append{}(VarI:K{},VarDotVar1:K{})),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{Id{}, K{}}(VarX:Id{}),VarI:K{}),VarDotVar2:Map{}))))))
[]
// rule `_orElseBool__BOOL__Bool_Bool`(#token("false","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(307) org.kframework.attributes.Location(Location(307,8,307,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("false"),VarK:Bool{}),
VarK:Bool{}),
\top{R}()))
[]
// rule isKItem(inj{Block,K}(Block))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Block{}, K{}}(VarBlock:Block{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_orBool__BOOL__Bool_Bool`(_7,#token("true","Bool"))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(301) org.kframework.attributes.Location(Location(301,8,301,34)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Var'Unds'7:Bool{},\dv{Bool{}}("true")),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_andBool_`(_4,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(288) org.kframework.attributes.Location(Location(288,8,288,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andBool'Unds'{}(Var'Unds'4:Bool{},\dv{Bool{}}("false")),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_andThenBool__BOOL__Bool_Bool`(#token("true","Bool"),K)=>K requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(290) org.kframework.attributes.Location(Location(290,8,290,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("true"),VarK:Bool{}),
VarK:Bool{}),
\top{R}()))
[]
// rule `replace(_,_,_,_)_STRING__String_String_String_Int`(Source,ToReplace,Replacement,Count)=>`_+String__STRING__String_String`(`_+String__STRING__String_String`(substrString(Source,#token("0","Int"),findString(Source,ToReplace,#token("0","Int"))),Replacement),`replace(_,_,_,_)_STRING__String_String_String_Int`(substrString(Source,`_+Int__INT__Int_Int`(findString(Source,ToReplace,#token("0","Int")),lengthString(ToReplace)),lengthString(Source)),ToReplace,Replacement,`_-Int__INT__Int_Int`(Count,#token("1","Int")))) requires `_>Int__INT__Int_Int`(Count,#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(549) org.kframework.attributes.Location(Location(549,8,552,30)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-GT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarCount:Int{},\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{String{},R} (
Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(VarSource:String{},VarToReplace:String{},VarReplacement:String{},VarCount:Int{}),
Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(LblsubstrString{}(VarSource:String{},\dv{Int{}}("0"),LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0"))),VarReplacement:String{}),Lblreplace'LParUndsCommUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String'Unds'Int{}(LblsubstrString{}(VarSource:String{},Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0")),LbllengthString{}(VarToReplace:String{})),LbllengthString{}(VarSource:String{})),VarToReplace:String{},VarReplacement:String{},Lbl'Unds'-Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarCount:Int{},\dv{Int{}}("1"))))),
\top{R}()))
[]
// rule isPgm(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarPgm:Pgm{},
\and{Bool{}} (
\top{Bool{}}(),
LblisPgm{}(inj{Pgm{}, K{}}(VarPgm:Pgm{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisPgm{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_>String__STRING__String_String`(S1,S2)=>`_<String__STRING__String_String`(S2,S1) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(529) org.kframework.attributes.Location(Location(529,8,529,52)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds-GT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}),
Lbl'Unds-LT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS2:String{},VarS1:String{})),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`!__IMP-SYNTAX__BExp`(HOLE))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezer!__IMP-SYNTAX__BExp0_`(.KList)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) heat() org.kframework.attributes.Location(Location(37,20,37,67)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(669003786) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(VarHOLE:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`___IMP-SYNTAX__Stmt_Stmt`(S1,S2))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(S1)~>inj{Stmt,KItem}(S2)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(173) org.kframework.attributes.Location(Location(173,8,173,35)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K) structural()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(VarS1:Stmt{},VarS2:Stmt{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(VarS1:Stmt{}),kseq{}(inj{Stmt{}, KItem{}}(VarS2:Stmt{}),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `_orElseBool__BOOL__Bool_Bool`(K,#token("false","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(308) org.kframework.attributes.Location(Location(308,8,308,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarK:Bool{},\dv{Bool{}}("false")),
VarK:Bool{}),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`_+__IMP-SYNTAX__AExp_AExp`(inj{Int,AExp}(I1),inj{Int,AExp}(I2)))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Int,KItem}(`_+Int__INT__Int_Int`(I1,I2))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(122) org.kframework.attributes.Location(Location(122,8,122,29)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl'UndsPlusUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(inj{Int{}, AExp{}}(VarI1:Int{}),inj{Int{}, AExp{}}(VarI2:Int{}))),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Int{}, KItem{}}(Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_xorBool__BOOL__Bool_Bool`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(296) org.kframework.attributes.Location(Location(296,8,296,38)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB:Bool{},\dv{Bool{}}("false")),
VarB:Bool{}),
\top{R}()))
[]
// rule isAExp(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarInt:Int{},
\and{Bool{}} (
\top{Bool{}}(),
LblisAExp{}(inj{Int{}, K{}}(VarInt:Int{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarAExp:AExp{},
\and{Bool{}} (
\top{Bool{}}(),
LblisAExp{}(inj{AExp{}, K{}}(VarAExp:AExp{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarId:Id{},
\and{Bool{}} (
\top{Bool{}}(),
LblisAExp{}(inj{Id{}, K{}}(VarId:Id{}))))),
\bottom{R}())))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisAExp{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_<=__IMP-SYNTAX__AExp_AExp1_`(inj{AExp,K}(K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(`_<=__IMP-SYNTAX__AExp_AExp`(HOLE,K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() latex({#1}\leq{#2}) org.kframework.attributes.Location(Location(36,20,36,91)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(242352470) seqstrict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp1'Unds'{}(inj{AExp{}, K{}}(VarK1:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarHOLE:AExp{},VarK1:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`_=_;_IMP-SYNTAX__Id_AExp`(X,inj{Int,AExp}(I)))~>DotVar1),`<state>`(`_Map_`(`_|->_`(inj{Id,K}(X),_20),DotVar2)))=>`<T>`(`<k>`(DotVar1),`<state>`(`_Map_`(`_|->_`(inj{Id,K}(X),inj{Int,K}(I)),DotVar2))) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(160) org.kframework.attributes.Location(Location(160,8,160,73)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(VarX:Id{},inj{Int{}, AExp{}}(VarI:Int{}))),VarDotVar1:K{})),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{Id{}, K{}}(VarX:Id{}),Var'Unds'20:K{}),VarDotVar2:Map{}))),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar1:K{}),Lbl'-LT-'state'-GT-'{}(Lbl'Unds'Map'Unds'{}(Lbl'UndsPipe'-'-GT-Unds'{}(inj{Id{}, K{}}(VarX:Id{}),inj{Int{}, K{}}(VarI:Int{})),VarDotVar2:Map{}))))))
[]
// rule isTCellFragment(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarTCellFragment:TCellFragment{},
\and{Bool{}} (
\top{Bool{}}(),
LblisTCellFragment{}(inj{TCellFragment{}, K{}}(VarTCellFragment:TCellFragment{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisTCellFragment{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isKItem(inj{Float,K}(Float))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Float{}, K{}}(VarFloat:Float{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isStateCellOpt(inj{StateCell,K}(StateCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisStateCellOpt{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{Cell,K}(Cell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Cell{}, K{}}(VarCell:Cell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{Stmt,K}(Stmt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Stmt{}, K{}}(VarStmt:Stmt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_<=__IMP-SYNTAX__AExp_AExp`(inj{Int,AExp}(I1),inj{Int,AExp}(I2)))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Bool,KItem}(`_<=Int__INT__Int_Int`(I1,I2))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(131) org.kframework.attributes.Location(Location(131,8,131,31)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(inj{Int{}, AExp{}}(VarI1:Int{}),inj{Int{}, AExp{}}(VarI2:Int{}))),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Bool{}, KItem{}}(Lbl'Unds-LT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_=/=K__K-EQUAL__K_K`(K1,K2)=>`notBool_`(`_==K_`(K1,K2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(626) org.kframework.attributes.Location(Location(626,8,626,45)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsSlshEqls'K'UndsUnds'K-EQUAL'UndsUnds'K'Unds'K{}(VarK1:K{},VarK2:K{}),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'K'Unds'{}(VarK1:K{},VarK2:K{}))),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_&&__IMP-SYNTAX__BExp_BExp`(inj{Bool,BExp}(#token("true","Bool")),B))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(B)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(133) org.kframework.attributes.Location(Location(133,8,133,22)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(inj{Bool{}, BExp{}}(\dv{Bool{}}("true")),VarB:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarB:BExp{}),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `#if_#then_#else_#fi_K-EQUAL__Bool_K_K`(C,B1,_10)=>B1 requires C ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(632) org.kframework.attributes.Location(Location(632,8,632,56)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
VarC:Bool{},
\dv{Bool{}}("true")),
\and{R} (
\equals{K{},R} (
Lbl'Hash'if'UndsHash'then'UndsHash'else'UndsHash'fi'Unds'K-EQUAL'UndsUnds'Bool'Unds'K'Unds'K{K{}}(VarC:Bool{},VarB1:K{},Var'Unds'10:K{}),
VarB1:K{}),
\top{R}()))
[]
// rule findChar(_12,#token("\"\"","String"),_13)=>#token("-1","Int") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(533) org.kframework.attributes.Location(Location(533,8,533,32)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Int{},R} (
LblfindChar{}(Var'Unds'12:String{},\dv{String{}}("\"\""),Var'Unds'13:Int{}),
\dv{Int{}}("-1")),
\top{R}()))
[]
// rule isKItem(inj{StateCell,K}(StateCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isCell(inj{TCell,K}(TCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisCell{}(inj{TCell{}, K{}}(VarTCell:TCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isInt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarInt:Int{},
\and{Bool{}} (
\top{Bool{}}(),
LblisInt{}(inj{Int{}, K{}}(VarInt:Int{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisInt{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isStateCell(inj{StateCell,K}(StateCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisStateCell{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKCellOpt(inj{KCellOpt,K}(KCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKCellOpt{}(inj{KCellOpt{}, K{}}(VarKCellOpt:KCellOpt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`while(_)__IMP-SYNTAX__BExp_Block`(B,S))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(`if(_)_else__IMP-SYNTAX__BExp_Block_Block`(B,`{_}_IMP-SYNTAX__Stmt`(`___IMP-SYNTAX__Stmt_Stmt`(inj{Block,Stmt}(S),`while(_)__IMP-SYNTAX__BExp_Block`(B,S))),`{}_IMP-SYNTAX_`(.KList)))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(189) org.kframework.attributes.Location(Location(189,8,189,53)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K) structural()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(VarB:BExp{},VarS:Block{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(VarB:BExp{},Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(Lbl'UndsUndsUnds'IMP-SYNTAX'UndsUnds'Stmt'Unds'Stmt{}(inj{Block{}, Stmt{}}(VarS:Block{}),Lblwhile'LParUndsRParUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block{}(VarB:BExp{},VarS:Block{}))),Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}())),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_impliesBool__BOOL__Bool_Bool`(#token("true","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(310) org.kframework.attributes.Location(Location(310,8,310,36)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("true"),VarB:Bool{}),
VarB:Bool{}),
\top{R}()))
[]
// rule `_impliesBool__BOOL__Bool_Bool`(#token("false","Bool"),_0)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(311) org.kframework.attributes.Location(Location(311,8,311,40)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'impliesBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("false"),Var'Unds'0:Bool{}),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{AExp,K}(AExp))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{AExp{}, K{}}(VarAExp:AExp{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isPgm(inj{Pgm,K}(Pgm))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisPgm{}(inj{Pgm{}, K{}}(VarPgm:Pgm{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule freshId(I)=>`String2Id`(`_+String__STRING__String_String`(#token("\"_\"","String"),`Int2String`(I))) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(608) org.kframework.attributes.Location(Location(608,8,608,62)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Id{},R} (
LblfreshId{}(VarI:Int{}),
LblString2Id{}(Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(\dv{String{}}("\"_\""),LblInt2String{}(VarI:Int{})))),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Block,KItem}(`{}_IMP-SYNTAX_`(.KList))~>DotVar1),DotVar0)=>`<T>`(`<k>`(DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(152) org.kframework.attributes.Location(Location(152,8,152,15)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K) structural()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Block{}, KItem{}}(Lbl'LBraRBraUnds'IMP-SYNTAX'Unds'{}()),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(VarDotVar1:K{}),VarDotVar0:StateCell{}))))
[]
// rule isKItem(inj{Set,K}(Set))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Set{}, K{}}(VarSet:Set{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezer_&&__IMP-SYNTAX__BExp_BExp1_`(inj{BExp,K}(K1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(`_&&__IMP-SYNTAX__BExp_BExp`(HOLE,K1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() left() org.kframework.attributes.Location(Location(38,20,38,76)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1616548737) strict(1)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezer'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp1'Unds'{}(inj{BExp{}, K{}}(VarK1:BExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(VarHOLE:BExp{},VarK1:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `replaceFirst(_,_,_)_STRING__String_String_String`(Source,ToReplace,_18)=>Source requires `_<Int__INT__Int_Int`(findString(Source,ToReplace,#token("0","Int")),#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(545) org.kframework.attributes.Location(Location(545,8,546,57)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-LT-'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0")),\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{String{},R} (
LblreplaceFirst'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(VarSource:String{},VarToReplace:String{},Var'Unds'18:String{}),
VarSource:String{}),
\top{R}()))
[]
// rule `_=/=String__STRING__String_String`(S1,S2)=>`notBool_`(`_==String__STRING__String_String`(S1,S2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(515) org.kframework.attributes.Location(Location(515,8,515,65)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsSlshEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}))),
\top{R}()))
[]
// rule isInt(inj{Int,K}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisInt{}(inj{Int{}, K{}}(VarInt:Int{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isAExp(inj{Id,K}(Id))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisAExp{}(inj{Id{}, K{}}(VarId:Id{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStmt:Stmt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Stmt{}, K{}}(VarStmt:Stmt{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCell:StateCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarPgm:Pgm{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Pgm{}, K{}}(VarPgm:Pgm{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCellOpt:KCellOpt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{KCellOpt{}, K{}}(VarKCellOpt:KCellOpt{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCell:KCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{KCell{}, K{}}(VarKCell:KCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarSet:Set{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Set{}, K{}}(VarSet:Set{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarInt:Int{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Int{}, K{}}(VarInt:Int{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCellOpt:StateCellOpt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{StateCellOpt{}, K{}}(VarStateCellOpt:StateCellOpt{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarTCell:TCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{TCell{}, K{}}(VarTCell:TCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarFloat:Float{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Float{}, K{}}(VarFloat:Float{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarMap:Map{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Map{}, K{}}(VarMap:Map{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarList:List{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{List{}, K{}}(VarList:List{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarCell:Cell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Cell{}, K{}}(VarCell:Cell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarAExp:AExp{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{AExp{}, K{}}(VarAExp:AExp{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarIds:Ids{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Ids{}, K{}}(VarIds:Ids{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBlock:Block{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Block{}, K{}}(VarBlock:Block{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarTCellFragment:TCellFragment{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{TCellFragment{}, K{}}(VarTCellFragment:TCellFragment{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarString:String{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{String{}, K{}}(VarString:String{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarId:Id{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Id{}, K{}}(VarId:Id{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKResult:KResult{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{KResult{}, K{}}(VarKResult:KResult{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBExp:BExp{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{BExp{}, K{}}(VarBExp:BExp{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBool:Bool{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{Bool{}, K{}}(VarBool:Bool{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKItem:KItem{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKItem{}(inj{KItem{}, K{}}(VarKItem:KItem{}))))),
\bottom{R}())))))))))))))))))))))))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isKItem(inj{String,K}(String))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{String{}, K{}}(VarString:String{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{Pgm,K}(Pgm))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Pgm{}, K{}}(VarPgm:Pgm{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{Map,K}(Map))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Map{}, K{}}(VarMap:Map{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isStmt(inj{Block,K}(Block))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisStmt{}(inj{Block{}, K{}}(VarBlock:Block{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_andThenBool__BOOL__Bool_Bool`(_2,#token("false","Bool"))=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(293) org.kframework.attributes.Location(Location(293,8,293,36)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(Var'Unds'2:Bool{},\dv{Bool{}}("false")),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isKItem(inj{TCellFragment,K}(TCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{TCellFragment{}, K{}}(VarTCellFragment:TCellFragment{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKItem(inj{Bool,K}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Bool{}, K{}}(VarBool:Bool{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKResult(inj{KResult,K}(KResult))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKResult{}(inj{KResult{}, K{}}(VarKResult:KResult{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isTCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarTCell:TCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisTCell{}(inj{TCell{}, K{}}(VarTCell:TCell{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisTCell{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isBlock(inj{Block,K}(Block))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisBlock{}(inj{Block{}, K{}}(VarBlock:Block{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isList(inj{List,K}(List))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisList{}(inj{List{}, K{}}(VarList:List{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_orElseBool__BOOL__Bool_Bool`(#token("true","Bool"),_8)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(305) org.kframework.attributes.Location(Location(305,8,305,33)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orElseBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("true"),Var'Unds'8:Bool{}),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isStmt(inj{Stmt,K}(Stmt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisStmt{}(inj{Stmt{}, K{}}(VarStmt:Stmt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isBool(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBool:Bool{},
\and{Bool{}} (
\top{Bool{}}(),
LblisBool{}(inj{Bool{}, K{}}(VarBool:Bool{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisBool{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isBExp(inj{Bool,K}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisBExp{}(inj{Bool{}, K{}}(VarBool:Bool{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule rfindChar(_16,#token("\"\"","String"),_17)=>#token("-1","Int") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(535) org.kframework.attributes.Location(Location(535,8,535,33)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Int{},R} (
LblrfindChar{}(Var'Unds'16:String{},\dv{String{}}("\"\""),Var'Unds'17:Int{}),
\dv{Int{}}("-1")),
\top{R}()))
[]
// rule `_andThenBool__BOOL__Bool_Bool`(#token("false","Bool"),_1)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(292) org.kframework.attributes.Location(Location(292,8,292,36)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("false"),Var'Unds'1:Bool{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_=/=Bool__BOOL__Bool_Bool`(B1,B2)=>`notBool_`(`_==Bool__BOOL__Bool_Bool`(B1,B2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(315) org.kframework.attributes.Location(Location(315,8,315,57)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsSlshEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB1:Bool{},VarB2:Bool{}),
LblnotBool'Unds'{}(Lbl'UndsEqlsEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB1:Bool{},VarB2:Bool{}))),
\top{R}()))
[]
// rule isKCellOpt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCellOpt:KCellOpt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKCellOpt{}(inj{KCellOpt{}, K{}}(VarKCellOpt:KCellOpt{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCell:KCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKCellOpt{}(inj{KCell{}, K{}}(VarKCell:KCell{}))))),
\bottom{R}()))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisKCellOpt{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule isString(inj{String,K}(String))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisString{}(inj{String{}, K{}}(VarString:String{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`if(_)_else__IMP-SYNTAX__BExp_Block_Block`(inj{Bool,BExp}(#token("false","Bool")),_22,S))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Block,KItem}(S)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(183) org.kframework.attributes.Location(Location(183,8,183,32)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(inj{Bool{}, BExp{}}(\dv{Bool{}}("false")),Var'Unds'22:Block{},VarS:Block{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Block{}, KItem{}}(VarS:Block{}),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `<T>`(`<k>`(inj{Pgm,KItem}(`int_;__IMP-SYNTAX__Ids_Stmt`(`.List{"_,__IMP-SYNTAX_"}_Ids`(.KList),S))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(S)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(206) org.kframework.attributes.Location(Location(206,8,206,24)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K) structural()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Pgm{}, KItem{}}(Lblint'UndsSClnUndsUnds'IMP-SYNTAX'UndsUnds'Ids'Unds'Stmt{}(Lbl'Stop'List'LBraQuotUndsCommUndsUnds'IMP-SYNTAX'UndsQuotRBraUnds'Ids{}(),VarS:Stmt{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(VarS:Stmt{}),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_==String__STRING__String_String`(S1,S2)=>`_==K_`(inj{String,K}(S1),inj{String,K}(S2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(516) org.kframework.attributes.Location(Location(516,8,516,49)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsEqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}),
Lbl'UndsEqlsEqls'K'Unds'{}(inj{String{}, K{}}(VarS1:String{}),inj{String{}, K{}}(VarS2:String{}))),
\top{R}()))
[]
// rule `_==Int_`(I1,I2)=>`_==K_`(inj{Int,K}(I1),inj{Int,K}(I2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(382) org.kframework.attributes.Location(Location(382,8,382,40)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsEqls'Int'Unds'{}(VarI1:Int{},VarI2:Int{}),
Lbl'UndsEqlsEqls'K'Unds'{}(inj{Int{}, K{}}(VarI1:Int{}),inj{Int{}, K{}}(VarI2:Int{}))),
\top{R}()))
[]
// rule isMap(inj{Map,K}(Map))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisMap{}(inj{Map{}, K{}}(VarMap:Map{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule initKCell(Init)=>`<k>`(`Map:lookup`(Init,inj{KConfigVar,K}(#token("$PGM","KConfigVar")))) requires #token("true","Bool") ensures #token("true","Bool") [initializer()]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{KCell{},R} (
LblinitKCell{}(VarInit:Map{}),
Lbl'-LT-'k'-GT-'{}(LblMap'Coln'lookup{}(VarInit:Map{},inj{KConfigVar{}, K{}}(\dv{KConfigVar{}}("$PGM"))))),
\top{R}()))
[]
// rule initStateCell(.KList)=>`<state>`(`.Map`(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [initializer()]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{StateCell{},R} (
LblinitStateCell{}(),
Lbl'-LT-'state'-GT-'{}(Lbl'Stop'Map{}())),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_<=__IMP-SYNTAX__AExp_AExp`(K0,HOLE))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_<=__IMP-SYNTAX__AExp_AExp0_`(inj{AExp,K}(K0))~>DotVar1),DotVar0) requires isKResult(inj{AExp,K}(K0)) ensures #token("true","Bool") [color(pink) heat() latex({#1}\leq{#2}) org.kframework.attributes.Location(Location(36,20,36,91)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(242352470) seqstrict()]
axiom{} \and{TCell{}} (
\equals{Bool{},TCell{}}(
LblisKResult{}(inj{AExp{}, K{}}(VarK0:AExp{})),
\dv{Bool{}}("true")), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp{}(VarK0:AExp{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'Unds-LT-EqlsUndsUnds'IMP-SYNTAX'UndsUnds'AExp'Unds'AExp0'Unds'{}(inj{AExp{}, K{}}(VarK0:AExp{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`_&&__IMP-SYNTAX__BExp_BExp`(inj{Bool,BExp}(#token("false","Bool")),_21))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Bool,KItem}(#token("false","Bool"))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(134) org.kframework.attributes.Location(Location(134,8,134,27)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'UndsAndAndUndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'BExp{}(inj{Bool{}, BExp{}}(\dv{Bool{}}("false")),Var'Unds'21:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Bool{}, KItem{}}(\dv{Bool{}}("false")),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule freshInt(I)=>I requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(387) org.kframework.attributes.Location(Location(387,8,387,28)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Int{},R} (
LblfreshInt{}(VarI:Int{}),
VarI:Int{}),
\top{R}()))
[]
// rule isString(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarString:String{},
\and{Bool{}} (
\top{Bool{}}(),
LblisString{}(inj{String{}, K{}}(VarString:String{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisString{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Block,KItem}(`{_}_IMP-SYNTAX__Stmt`(S))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(S)~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(153) org.kframework.attributes.Location(Location(153,8,153,16)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K) structural()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Block{}, KItem{}}(Lbl'LBraUndsRBraUnds'IMP-SYNTAX'UndsUnds'Stmt{}(VarS:Stmt{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(VarS:Stmt{}),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isKItem(inj{StateCellOpt,K}(StateCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{StateCellOpt{}, K{}}(VarStateCellOpt:StateCellOpt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isId(inj{Id,K}(Id))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisId{}(inj{Id{}, K{}}(VarId:Id{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isStmt(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBlock:Block{},
\and{Bool{}} (
\top{Bool{}}(),
LblisStmt{}(inj{Block{}, K{}}(VarBlock:Block{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStmt:Stmt{},
\and{Bool{}} (
\top{Bool{}}(),
LblisStmt{}(inj{Stmt{}, K{}}(VarStmt:Stmt{}))))),
\bottom{R}()))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisStmt{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_xorBool__BOOL__Bool_Bool`(#token("false","Bool"),B)=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(295) org.kframework.attributes.Location(Location(295,8,295,38)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'xorBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("false"),VarB:Bool{}),
VarB:Bool{}),
\top{R}()))
[]
// rule isKItem(inj{Int,K}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{Int{}, K{}}(VarInt:Int{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isTCellFragment(inj{TCellFragment,K}(TCellFragment))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisTCellFragment{}(inj{TCellFragment{}, K{}}(VarTCellFragment:TCellFragment{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarStateCell:StateCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisCell{}(inj{StateCell{}, K{}}(VarStateCell:StateCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarCell:Cell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisCell{}(inj{Cell{}, K{}}(VarCell:Cell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCell:KCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisCell{}(inj{KCell{}, K{}}(VarKCell:KCell{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarTCell:TCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisCell{}(inj{TCell{}, K{}}(VarTCell:TCell{}))))),
\bottom{R}()))))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisCell{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(`!__IMP-SYNTAX__BExp`(inj{Bool,BExp}(T)))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Bool,KItem}(`notBool_`(T))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(132) org.kframework.attributes.Location(Location(132,8,132,24)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(inj{Bool{}, BExp{}}(VarT:Bool{}))),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Bool{}, KItem{}}(LblnotBool'Unds'{}(VarT:Bool{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isCell(inj{KCell,K}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisCell{}(inj{KCell{}, K{}}(VarKCell:KCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(`-__IMP-SYNTAX__Int`(I1))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Int,KItem}(`_-Int__INT__Int_Int`(#token("0","Int"),I1))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(123) org.kframework.attributes.Location(Location(123,8,123,25)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(Lbl-'UndsUnds'IMP-SYNTAX'UndsUnds'Int{}(VarI1:Int{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Int{}, KItem{}}(Lbl'Unds'-Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(\dv{Int{}}("0"),VarI1:Int{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule isStateCellOpt(inj{StateCellOpt,K}(StateCellOpt))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisStateCellOpt{}(inj{StateCellOpt{}, K{}}(VarStateCellOpt:StateCellOpt{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKCellOpt(inj{KCell,K}(KCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKCellOpt{}(inj{KCell{}, K{}}(VarKCell:KCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isKResult(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarInt:Int{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKResult{}(inj{Int{}, K{}}(VarInt:Int{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarBool:Bool{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKResult{}(inj{Bool{}, K{}}(VarBool:Bool{}))))),
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKResult:KResult{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKResult{}(inj{KResult{}, K{}}(VarKResult:KResult{}))))),
\bottom{R}())))),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisKResult{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_orBool__BOOL__Bool_Bool`(B,#token("false","Bool"))=>B requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(303) org.kframework.attributes.Location(Location(303,8,303,32)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarB:Bool{},\dv{Bool{}}("false")),
VarB:Bool{}),
\top{R}()))
[]
// rule isBool(inj{Bool,K}(Bool))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisBool{}(inj{Bool{}, K{}}(VarBool:Bool{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_modInt__INT__Int_Int`(I1,I2)=>`_%Int__INT__Int_Int`(`_+Int__INT__Int_Int`(`_%Int__INT__Int_Int`(I1,absInt(I2)),absInt(I2)),absInt(I2)) requires `_=/=Int__INT__Int_Int`(I2,#token("0","Int")) ensures #token("true","Bool") [concrete() contentStartColumn(5) contentStartLine(366) org.kframework.attributes.Location(Location(366,5,369,23)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI2:Int{},\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
Lbl'Unds'modInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
Lbl'UndsPerc'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Lbl'UndsPerc'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},LblabsInt{}(VarI2:Int{})),LblabsInt{}(VarI2:Int{})),LblabsInt{}(VarI2:Int{}))),
\top{R}()))
[]
// rule `replaceFirst(_,_,_)_STRING__String_String_String`(Source,ToReplace,Replacement)=>`_+String__STRING__String_String`(`_+String__STRING__String_String`(substrString(Source,#token("0","Int"),findString(Source,ToReplace,#token("0","Int"))),Replacement),substrString(Source,`_+Int__INT__Int_Int`(findString(Source,ToReplace,#token("0","Int")),lengthString(ToReplace)),lengthString(Source))) requires `_>=Int__INT__Int_Int`(findString(Source,ToReplace,#token("0","Int")),#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(542) org.kframework.attributes.Location(Location(542,8,544,66)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-GT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0")),\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{String{},R} (
LblreplaceFirst'LParUndsCommUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String'Unds'String{}(VarSource:String{},VarToReplace:String{},VarReplacement:String{}),
Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(Lbl'UndsPlus'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(LblsubstrString{}(VarSource:String{},\dv{Int{}}("0"),LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0"))),VarReplacement:String{}),LblsubstrString{}(VarSource:String{},Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToReplace:String{},\dv{Int{}}("0")),LbllengthString{}(VarToReplace:String{})),LbllengthString{}(VarSource:String{})))),
\top{R}()))
[]
// rule isCell(inj{Cell,K}(Cell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisCell{}(inj{Cell{}, K{}}(VarCell:Cell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{AExp,KItem}(HOLE)~>`#freezer_=_;_IMP-SYNTAX__Id_AExp0_`(inj{Id,K}(K0))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{Stmt,KItem}(`_=_;_IMP-SYNTAX__Id_AExp`(K0,HOLE))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() format(%1 %2 %3%4) org.kframework.attributes.Location(Location(43,20,43,90)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1983769324) strict(2)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{AExp{}, KItem{}}(VarHOLE:AExp{}),kseq{}(Lbl'Hash'freezer'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp0'Unds'{}(inj{Id{}, K{}}(VarK0:Id{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lbl'UndsEqlsUndsSClnUnds'IMP-SYNTAX'UndsUnds'Id'Unds'AExp{}(VarK0:Id{},VarHOLE:AExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `countAllOccurrences(_,_)_STRING__String_String`(Source,ToCount)=>`_+Int__INT__Int_Int`(#token("1","Int"),`countAllOccurrences(_,_)_STRING__String_String`(substrString(Source,`_+Int__INT__Int_Int`(findString(Source,ToCount,#token("0","Int")),lengthString(ToCount)),lengthString(Source)),ToCount)) requires `_>=Int__INT__Int_Int`(findString(Source,ToCount,#token("0","Int")),#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(539) org.kframework.attributes.Location(Location(539,8,540,60)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-GT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToCount:String{},\dv{Int{}}("0")),\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(VarSource:String{},VarToCount:String{}),
Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(\dv{Int{}}("1"),LblcountAllOccurrences'LParUndsCommUndsRParUnds'STRING'UndsUnds'String'Unds'String{}(LblsubstrString{}(VarSource:String{},Lbl'UndsPlus'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(LblfindString{}(VarSource:String{},VarToCount:String{},\dv{Int{}}("0")),LbllengthString{}(VarToCount:String{})),LbllengthString{}(VarSource:String{})),VarToCount:String{}))),
\top{R}()))
[]
// rule isKCell(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKCell:KCell{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKCell{}(inj{KCell{}, K{}}(VarKCell:KCell{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisKCell{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule initTCell(Init)=>`<T>`(initKCell(Init),initStateCell(.KList)) requires #token("true","Bool") ensures #token("true","Bool") [initializer()]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{TCell{},R} (
LblinitTCell{}(VarInit:Map{}),
Lbl'-LT-'T'-GT-'{}(LblinitKCell{}(VarInit:Map{}),LblinitStateCell{}())),
\top{R}()))
[]
// rule `minInt(_,_)_INT__Int_Int`(I1,I2)=>I2 requires `_>=Int__INT__Int_Int`(I1,I2) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(372) org.kframework.attributes.Location(Location(372,8,372,57)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'Unds-GT-Eqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
LblminInt'LParUndsCommUndsRParUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
VarI2:Int{}),
\top{R}()))
[]
// rule `_==Bool__BOOL__Bool_Bool`(K1,K2)=>`_==K_`(inj{Bool,K}(K1),inj{Bool,K}(K2)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(628) org.kframework.attributes.Location(Location(628,8,628,43)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'UndsEqlsEqls'Bool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarK1:Bool{},VarK2:Bool{}),
Lbl'UndsEqlsEqls'K'Unds'{}(inj{Bool{}, K{}}(VarK1:Bool{}),inj{Bool{}, K{}}(VarK2:Bool{}))),
\top{R}()))
[]
// rule isKResult(inj{Int,K}(Int))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKResult{}(inj{Int{}, K{}}(VarInt:Int{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_<=String__STRING__String_String`(S1,S2)=>`notBool_`(`_<String__STRING__String_String`(S2,S1)) requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(528) org.kframework.attributes.Location(Location(528,8,528,63)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds-LT-Eqls'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS1:String{},VarS2:String{}),
LblnotBool'Unds'{}(Lbl'Unds-LT-'String'UndsUnds'STRING'UndsUnds'String'Unds'String{}(VarS2:String{},VarS1:String{}))),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezer!__IMP-SYNTAX__BExp0_`(.KList)~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(`!__IMP-SYNTAX__BExp`(HOLE))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [color(pink) cool() org.kframework.attributes.Location(Location(37,20,37,67)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(669003786) strict()]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezer'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp0'Unds'{}(),VarDotVar1:K{}))),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(Lbl'BangUndsUnds'IMP-SYNTAX'UndsUnds'BExp{}(VarHOLE:BExp{})),VarDotVar1:K{})),VarDotVar0:StateCell{}))))
[]
// rule `_orBool__BOOL__Bool_Bool`(#token("true","Bool"),_5)=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(300) org.kframework.attributes.Location(Location(300,8,300,34)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'orBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(\dv{Bool{}}("true"),Var'Unds'5:Bool{}),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule `_andThenBool__BOOL__Bool_Bool`(K,#token("true","Bool"))=>K requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(291) org.kframework.attributes.Location(Location(291,8,291,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andThenBool'UndsUnds'BOOL'UndsUnds'Bool'Unds'Bool{}(VarK:Bool{},\dv{Bool{}}("true")),
VarK:Bool{}),
\top{R}()))
[]
// rule `<T>`(`<k>`(inj{Stmt,KItem}(`if(_)_else__IMP-SYNTAX__BExp_Block_Block`(HOLE,K1,K2))~>DotVar1),DotVar0)=>`<T>`(`<k>`(inj{BExp,KItem}(HOLE)~>`#freezerif(_)_else__IMP-SYNTAX__BExp_Block_Block1_`(inj{Block,K}(K1),inj{Block,K}(K2))~>DotVar1),DotVar0) requires #token("true","Bool") ensures #token("true","Bool") [colors(yellow, white, white, yellow) format(%1 %2%3%4 %5 %6 %7) heat() org.kframework.attributes.Location(Location(44,20,45,123)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/tutorial/1_k/2_imp/lesson_5/imp.k)) productionID(1027937315) strict(1)]
axiom{} \and{TCell{}} (
\top{TCell{}}(), \and{TCell{}} (
\top{TCell{}}(), \rewrites{TCell{}}(Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{Stmt{}, KItem{}}(Lblif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block{}(VarHOLE:BExp{},VarK1:Block{},VarK2:Block{})),VarDotVar1:K{})),VarDotVar0:StateCell{}),Lbl'-LT-'T'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(inj{BExp{}, KItem{}}(VarHOLE:BExp{}),kseq{}(Lbl'Hash'freezerif'LParUndsRParUnds'else'UndsUnds'IMP-SYNTAX'UndsUnds'BExp'Unds'Block'Unds'Block1'Unds'{}(inj{Block{}, K{}}(VarK1:Block{}),inj{Block{}, K{}}(VarK2:Block{})),VarDotVar1:K{}))),VarDotVar0:StateCell{}))))
[]
// rule isKConfigVar(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarKConfigVar:KConfigVar{},
\and{Bool{}} (
\top{Bool{}}(),
LblisKConfigVar{}(inj{KConfigVar{}, K{}}(VarKConfigVar:KConfigVar{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisKConfigVar{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_divInt__INT__Int_Int`(I1,I2)=>`_/Int__INT__Int_Int`(`_-Int__INT__Int_Int`(I1,`_modInt__INT__Int_Int`(I1,I2)),I2) requires `_=/=Int__INT__Int_Int`(I2,#token("0","Int")) ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(363) org.kframework.attributes.Location(Location(363,8,364,23)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K "requires" K)]
axiom{R} \implies{R} (
\equals{Bool{},R}(
Lbl'UndsEqlsSlshEqls'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI2:Int{},\dv{Int{}}("0")),
\dv{Bool{}}("true")),
\and{R} (
\equals{Int{},R} (
Lbl'Unds'divInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{}),
Lbl'UndsSlsh'Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(Lbl'Unds'-Int'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},Lbl'Unds'modInt'UndsUnds'INT'UndsUnds'Int'Unds'Int{}(VarI1:Int{},VarI2:Int{})),VarI2:Int{})),
\top{R}()))
[]
// rule isKItem(inj{TCell,K}(TCell))=>#token("true","Bool") requires #token("true","Bool") ensures #token("true","Bool") []
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
LblisKItem{}(inj{TCell{}, K{}}(VarTCell:TCell{})),
\dv{Bool{}}("true")),
\top{R}()))
[]
// rule isId(K)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [owise()]
axiom{R} \implies{R} (
\and{R} (
\not{R} (
\or{R} (
\ceil{Bool{},R} (
\exists{Bool{}} (VarId:Id{},
\and{Bool{}} (
\top{Bool{}}(),
LblisId{}(inj{Id{}, K{}}(VarId:Id{}))))),
\bottom{R}())),
\top{R}()),
\and{R} (
\equals{Bool{},R} (
LblisId{}(VarK:K{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
// rule `_andBool_`(#token("false","Bool"),_9)=>#token("false","Bool") requires #token("true","Bool") ensures #token("true","Bool") [contentStartColumn(8) contentStartLine(287) org.kframework.attributes.Location(Location(287,8,287,37)) org.kframework.attributes.Source(Source(/home/dwightguth/k/k-distribution/include/builtin/domains.k)) org.kframework.definition.Production(syntax RuleContent ::= K)]
axiom{R} \implies{R} (
\top{R}(),
\and{R} (
\equals{Bool{},R} (
Lbl'Unds'andBool'Unds'{}(\dv{Bool{}}("false"),Var'Unds'9:Bool{}),
\dv{Bool{}}("false")),
\top{R}()))
[]
endmodule []
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment