inductive SortStatusCode : Type

• «.StatusCode_NETWORK_StatusCode» : SortStatusCode
• EVMC_INTERNAL_ERROR_NETWORK_StatusCode : SortStatusCode
• EVMC_REJECTED_NETWORK_StatusCode : SortStatusCode

instance instBEqSortStatusCode : BEq SortStatusCode

Equations

• instBEqSortStatusCode = { beq := beqSortStatusCode✝ }

instance instDecidableEqSortStatusCode : DecidableEq SortStatusCode

Equations

• instDecidableEqSortStatusCode x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortTernStackOp : Type

• ADDMOD_EVM_TernStackOp : SortTernStackOp
• MULMOD_EVM_TernStackOp : SortTernStackOp

instance instBEqSortTernStackOp : BEq SortTernStackOp

Equations

• instBEqSortTernStackOp = { beq := beqSortTernStackOp✝ }

instance instDecidableEqSortTernStackOp : DecidableEq SortTernStackOp

Equations

• instDecidableEqSortTernStackOp x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortNullStackOp : Type

• ADDRESS_EVM_NullStackOp : SortNullStackOp
• CALLER_EVM_NullStackOp : SortNullStackOp
• CHAINID_EVM_NullStackOp : SortNullStackOp
• COINBASE_EVM_NullStackOp : SortNullStackOp
• GASLIMIT_EVM_NullStackOp : SortNullStackOp
• GASPRICE_EVM_NullStackOp : SortNullStackOp
• NUMBER_EVM_NullStackOp : SortNullStackOp
• ORIGIN_EVM_NullStackOp : SortNullStackOp
• PC_EVM_NullStackOp : SortNullStackOp
• PREVRANDAO_EVM_NullStackOp : SortNullStackOp
• SELFBALANCE_EVM_NullStackOp : SortNullStackOp
• TIMESTAMP_EVM_NullStackOp : SortNullStackOp

instance instBEqSortNullStackOp : BEq SortNullStackOp

Equations

• instBEqSortNullStackOp = { beq := beqSortNullStackOp✝ }

instance instDecidableEqSortNullStackOp : DecidableEq SortNullStackOp

Equations

• instDecidableEqSortNullStackOp x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortScheduleConst : Type

• Gaccesslistaddress_SCHEDULE_ScheduleConst : SortScheduleConst
• Gaccessliststoragekey_SCHEDULE_ScheduleConst : SortScheduleConst
• Gbalance_SCHEDULE_ScheduleConst : SortScheduleConst
• Gbase_SCHEDULE_ScheduleConst : SortScheduleConst
• Gblockhash_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcall_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcallstipend_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcallvalue_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcodedeposit_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcoldaccountaccess_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcoldsload_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcopy_SCHEDULE_ScheduleConst : SortScheduleConst
• Gcreate_SCHEDULE_ScheduleConst : SortScheduleConst
• Gecadd_SCHEDULE_ScheduleConst : SortScheduleConst
• Gecmul_SCHEDULE_ScheduleConst : SortScheduleConst
• Gecpaircoeff_SCHEDULE_ScheduleConst : SortScheduleConst
• Gecpairconst_SCHEDULE_ScheduleConst : SortScheduleConst
• Gexp_SCHEDULE_ScheduleConst : SortScheduleConst
• Gexpbyte_SCHEDULE_ScheduleConst : SortScheduleConst
• Gextcodecopy_SCHEDULE_ScheduleConst : SortScheduleConst
• Gextcodesize_SCHEDULE_ScheduleConst : SortScheduleConst
• Gfround_SCHEDULE_ScheduleConst : SortScheduleConst
• Ghigh_SCHEDULE_ScheduleConst : SortScheduleConst
• Ginitcodewordcost_SCHEDULE_ScheduleConst : SortScheduleConst
• Gjumpdest_SCHEDULE_ScheduleConst : SortScheduleConst
• Glog_SCHEDULE_ScheduleConst : SortScheduleConst
• Glogdata_SCHEDULE_ScheduleConst : SortScheduleConst
• Glogtopic_SCHEDULE_ScheduleConst : SortScheduleConst
• Glow_SCHEDULE_ScheduleConst : SortScheduleConst
• Gmemory_SCHEDULE_ScheduleConst : SortScheduleConst
• Gmid_SCHEDULE_ScheduleConst : SortScheduleConst
• Gnewaccount_SCHEDULE_ScheduleConst : SortScheduleConst
• Gpointeval_SCHEDULE_ScheduleConst : SortScheduleConst
• Gquadcoeff_SCHEDULE_ScheduleConst : SortScheduleConst
• Gquaddivisor_SCHEDULE_ScheduleConst : SortScheduleConst
• Gselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
• Gsha3_SCHEDULE_ScheduleConst : SortScheduleConst
• Gsha3word_SCHEDULE_ScheduleConst : SortScheduleConst
• Gsload_SCHEDULE_ScheduleConst : SortScheduleConst
• Gsstorereset_SCHEDULE_ScheduleConst : SortScheduleConst
• Gsstoreset_SCHEDULE_ScheduleConst : SortScheduleConst
• Gtransaction_SCHEDULE_ScheduleConst : SortScheduleConst
• Gtxcreate_SCHEDULE_ScheduleConst : SortScheduleConst
• Gtxdatanonzero_SCHEDULE_ScheduleConst : SortScheduleConst
• Gtxdatazero_SCHEDULE_ScheduleConst : SortScheduleConst
• Gverylow_SCHEDULE_ScheduleConst : SortScheduleConst
• Gwarmstoragedirtystore_SCHEDULE_ScheduleConst : SortScheduleConst
• Gwarmstorageread_SCHEDULE_ScheduleConst : SortScheduleConst
• Gzero_SCHEDULE_ScheduleConst : SortScheduleConst
• Rb_SCHEDULE_ScheduleConst : SortScheduleConst
• Rmaxquotient_SCHEDULE_ScheduleConst : SortScheduleConst
• Rselfdestruct_SCHEDULE_ScheduleConst : SortScheduleConst
• Rsstoreclear_SCHEDULE_ScheduleConst : SortScheduleConst
• maxCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst
• maxInitCodeSize_SCHEDULE_ScheduleConst : SortScheduleConst

instance instBEqSortScheduleConst : BEq SortScheduleConst

Equations

• instBEqSortScheduleConst = { beq := beqSortScheduleConst✝ }

instance instDecidableEqSortScheduleConst : DecidableEq SortScheduleConst

Equations

• instDecidableEqSortScheduleConst x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortPushOp : Type

• PUSHZERO_EVM_PushOp : SortPushOp

instance instBEqSortPushOp : BEq SortPushOp

Equations

• instBEqSortPushOp = { beq := beqSortPushOp✝ }

instance instDecidableEqSortPushOp : DecidableEq SortPushOp

Equations

• instDecidableEqSortPushOp x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortSchedule : Type

• BERLIN_EVM : SortSchedule
• BYZANTIUM_EVM : SortSchedule
• CANCUN_EVM : SortSchedule
• CONSTANTINOPLE_EVM : SortSchedule
• DEFAULT_EVM : SortSchedule
• FRONTIER_EVM : SortSchedule
• HOMESTEAD_EVM : SortSchedule
• ISTANBUL_EVM : SortSchedule
• LONDON_EVM : SortSchedule
• MERGE_EVM : SortSchedule
• PETERSBURG_EVM : SortSchedule
• SHANGHAI_EVM : SortSchedule
• SPURIOUS_DRAGON_EVM : SortSchedule
• TANGERINE_WHISTLE_EVM : SortSchedule

instance instBEqSortSchedule : BEq SortSchedule

Equations

• instBEqSortSchedule = { beq := beqSortSchedule✝ }

instance instDecidableEqSortSchedule : DecidableEq SortSchedule

Equations

• instDecidableEqSortSchedule x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortUnStackOp : Type

• ISZERO_EVM_UnStackOp : SortUnStackOp
• MLOAD_EVM_UnStackOp : SortUnStackOp
• NOT_EVM_UnStackOp : SortUnStackOp
• SLOAD_EVM_UnStackOp : SortUnStackOp

instance instBEqSortUnStackOp : BEq SortUnStackOp

Equations

• instBEqSortUnStackOp = { beq := beqSortUnStackOp✝ }

instance instDecidableEqSortUnStackOp : DecidableEq SortUnStackOp

Equations

• instDecidableEqSortUnStackOp x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortTxType : Type

• «.TxType_EVM-TYPES_TxType» : SortTxType
• «AccessList_EVM-TYPES_TxType» : SortTxType
• «Blob_EVM-TYPES_TxType» : SortTxType
• «DynamicFee_EVM-TYPES_TxType» : SortTxType
• «Legacy_EVM-TYPES_TxType» : SortTxType

instance instBEqSortTxType : BEq SortTxType

Equations

• instBEqSortTxType = { beq := beqSortTxType✝ }

instance instDecidableEqSortTxType : DecidableEq SortTxType

Equations

• instDecidableEqSortTxType x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortScheduleFlag : Type

• Gemptyisnonexistent_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasaccesslist_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasbasefee_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasbeaconroot_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasblobbasefee_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasblobhash_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghaschainid_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghascreate2_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasdirtysstore_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghaseip6780_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasextcodehash_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasmaxinitcodesize_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasmcopy_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasprevrandao_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghaspushzero_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasrejectedfirstbyte_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasreturndata_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasrevert_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasselfbalance_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasshift_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghassstorestipend_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghasstaticcall_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghastransient_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghaswarmcoinbase_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Ghaswithdrawals_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Gselfdestructnewaccount_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Gstaticcalldepth_SCHEDULE_ScheduleFlag : SortScheduleFlag
• Gzerovaluenewaccountgas_SCHEDULE_ScheduleFlag : SortScheduleFlag

instance instBEqSortScheduleFlag : BEq SortScheduleFlag

Equations

• instBEqSortScheduleFlag = { beq := beqSortScheduleFlag✝ }

instance instDecidableEqSortScheduleFlag : DecidableEq SortScheduleFlag

Equations

• instDecidableEqSortScheduleFlag x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortBinStackOp : Type

• ADD_EVM_BinStackOp : SortBinStackOp
• AND_EVM_BinStackOp : SortBinStackOp
• BYTE_EVM_BinStackOp : SortBinStackOp
• DIV_EVM_BinStackOp : SortBinStackOp
• EQ_EVM_BinStackOp : SortBinStackOp
• EXP_EVM_BinStackOp : SortBinStackOp
• GT_EVM_BinStackOp : SortBinStackOp
• LT_EVM_BinStackOp : SortBinStackOp
• MOD_EVM_BinStackOp : SortBinStackOp
• MSTORE_EVM_BinStackOp : SortBinStackOp
• MSTORE8_EVM_BinStackOp : SortBinStackOp
• SAR_EVM_BinStackOp : SortBinStackOp
• SDIV_EVM_BinStackOp : SortBinStackOp
• SGT_EVM_BinStackOp : SortBinStackOp
• SHL_EVM_BinStackOp : SortBinStackOp
• SHR_EVM_BinStackOp : SortBinStackOp
• SIGNEXTEND_EVM_BinStackOp : SortBinStackOp
• SLT_EVM_BinStackOp : SortBinStackOp
• SMOD_EVM_BinStackOp : SortBinStackOp
• SSTORE_EVM_BinStackOp : SortBinStackOp
• SUB_EVM_BinStackOp : SortBinStackOp
• XOR_EVM_BinStackOp : SortBinStackOp

instance instBEqSortBinStackOp : BEq SortBinStackOp

Equations

• instBEqSortBinStackOp = { beq := beqSortBinStackOp✝ }

instance instDecidableEqSortBinStackOp : DecidableEq SortBinStackOp

Equations

• instDecidableEqSortBinStackOp x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

inductive SortMode : Type

• NORMAL : SortMode
• «SUCCESS_ETHEREUM-SIMULATION-PURE_Mode» : SortMode
• VMTESTS : SortMode

instance instBEqSortMode : BEq SortMode

Equations

• instBEqSortMode = { beq := beqSortMode✝ }

instance instDecidableEqSortMode : DecidableEq SortMode

Equations

• instDecidableEqSortMode x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure SortStatusCodeCell : Type

• val : SortStatusCode

instance instBEqSortStatusCodeCell : BEq SortStatusCodeCell

Equations

• instBEqSortStatusCodeCell = { beq := beqSortStatusCodeCell✝ }

instance instDecidableEqSortStatusCodeCell : DecidableEq SortStatusCodeCell

Equations

• instDecidableEqSortStatusCodeCell = decEqSortStatusCodeCell✝

structure SortScheduleCell : Type

• val : SortSchedule

instance instBEqSortScheduleCell : BEq SortScheduleCell

Equations

• instBEqSortScheduleCell = { beq := beqSortScheduleCell✝ }

instance instDecidableEqSortScheduleCell : DecidableEq SortScheduleCell

Equations

• instDecidableEqSortScheduleCell = decEqSortScheduleCell✝

structure SortTxTypeCell : Type

• val : SortTxType

instance instBEqSortTxTypeCell : BEq SortTxTypeCell

Equations

• instBEqSortTxTypeCell = { beq := beqSortTxTypeCell✝ }

instance instDecidableEqSortTxTypeCell : DecidableEq SortTxTypeCell

Equations

• instDecidableEqSortTxTypeCell = decEqSortTxTypeCell✝

structure SortBalanceCell : Type

• val : SortInt

instance instBEqSortBalanceCell : BEq SortBalanceCell

Equations

• instBEqSortBalanceCell = { beq := beqSortBalanceCell✝ }

instance instDecidableEqSortBalanceCell : DecidableEq SortBalanceCell

Equations

• instDecidableEqSortBalanceCell = decEqSortBalanceCell✝

structure SortCoinbaseCell : Type

• val : SortInt

instance instBEqSortCoinbaseCell : BEq SortCoinbaseCell

Equations

• instBEqSortCoinbaseCell = { beq := beqSortCoinbaseCell✝ }

instance instDecidableEqSortCoinbaseCell : DecidableEq SortCoinbaseCell

Equations

• instDecidableEqSortCoinbaseCell = decEqSortCoinbaseCell✝

structure SortBlockNonceCell : Type

• val : SortInt

instance instBEqSortBlockNonceCell : BEq SortBlockNonceCell

Equations

• instBEqSortBlockNonceCell = { beq := beqSortBlockNonceCell✝ }

instance instDecidableEqSortBlockNonceCell : DecidableEq SortBlockNonceCell

Equations

• instDecidableEqSortBlockNonceCell = decEqSortBlockNonceCell✝

structure SortTimestampCell : Type

• val : SortInt

instance instBEqSortTimestampCell : BEq SortTimestampCell

Equations

• instBEqSortTimestampCell = { beq := beqSortTimestampCell✝ }

instance instDecidableEqSortTimestampCell : DecidableEq SortTimestampCell

Equations

• instDecidableEqSortTimestampCell = decEqSortTimestampCell✝

structure SortPreviousHashCell : Type

• val : SortInt

instance instBEqSortPreviousHashCell : BEq SortPreviousHashCell

Equations

• instBEqSortPreviousHashCell = { beq := beqSortPreviousHashCell✝ }

instance instDecidableEqSortPreviousHashCell : DecidableEq SortPreviousHashCell

Equations

• instDecidableEqSortPreviousHashCell = decEqSortPreviousHashCell✝

structure SortValueCell : Type

• val : SortInt

instance instBEqSortValueCell : BEq SortValueCell

Equations

• instBEqSortValueCell = { beq := beqSortValueCell✝ }

instance instDecidableEqSortValueCell : DecidableEq SortValueCell

Equations

• instDecidableEqSortValueCell = decEqSortValueCell✝

structure SortRefundCell : Type

• val : SortInt

instance instBEqSortRefundCell : BEq SortRefundCell

Equations

• instBEqSortRefundCell = { beq := beqSortRefundCell✝ }

instance instDecidableEqSortRefundCell : DecidableEq SortRefundCell

Equations

• instDecidableEqSortRefundCell = decEqSortRefundCell✝

structure SortCallDepthCell : Type

• val : SortInt

instance instBEqSortCallDepthCell : BEq SortCallDepthCell

Equations

• instBEqSortCallDepthCell = { beq := beqSortCallDepthCell✝ }

instance instDecidableEqSortCallDepthCell : DecidableEq SortCallDepthCell

Equations

• instDecidableEqSortCallDepthCell = decEqSortCallDepthCell✝

structure SortBlobGasUsedCell : Type

• val : SortInt

instance instBEqSortBlobGasUsedCell : BEq SortBlobGasUsedCell

Equations

• instBEqSortBlobGasUsedCell = { beq := beqSortBlobGasUsedCell✝ }

instance instDecidableEqSortBlobGasUsedCell : DecidableEq SortBlobGasUsedCell

Equations

• instDecidableEqSortBlobGasUsedCell = decEqSortBlobGasUsedCell✝

inductive SortJSONKey : Type

• inj_SortInt (x : SortInt) : SortJSONKey

instance instBEqSortJSONKey : BEq SortJSONKey

Equations

• instBEqSortJSONKey = { beq := beqSortJSONKey✝ }

instance instDecidableEqSortJSONKey : DecidableEq SortJSONKey

Equations

• instDecidableEqSortJSONKey = decEqSortJSONKey✝

structure SortTxChainIDCell : Type

• val : SortInt

instance instBEqSortTxChainIDCell : BEq SortTxChainIDCell

Equations

• instBEqSortTxChainIDCell = { beq := beqSortTxChainIDCell✝ }

instance instDecidableEqSortTxChainIDCell : DecidableEq SortTxChainIDCell

Equations

• instDecidableEqSortTxChainIDCell = decEqSortTxChainIDCell✝

structure SortAcctIDCell : Type

• val : SortInt

instance instBEqSortAcctIDCell : BEq SortAcctIDCell

Equations

• instBEqSortAcctIDCell = { beq := beqSortAcctIDCell✝ }

instance instDecidableEqSortAcctIDCell : DecidableEq SortAcctIDCell

Equations

• instDecidableEqSortAcctIDCell = decEqSortAcctIDCell✝

inductive SortWordStack : Type

• «.WordStack_EVM-TYPES_WordStack» : SortWordStack
• «_:__EVM-TYPES_WordStack_Int_WordStack» (x0 : SortInt) (x1 : SortWordStack) : SortWordStack

instance instBEqSortWordStack : BEq SortWordStack

Equations

• instBEqSortWordStack = { beq := beqSortWordStack✝ }

instance instDecidableEqSortWordStack : DecidableEq SortWordStack

Equations

• instDecidableEqSortWordStack = decEqSortWordStack✝

structure SortGeneratedCounterCell : Type

• val : SortInt

instance instBEqSortGeneratedCounterCell : BEq SortGeneratedCounterCell

Equations

• instBEqSortGeneratedCounterCell = { beq := beqSortGeneratedCounterCell✝ }

instance instDecidableEqSortGeneratedCounterCell : DecidableEq SortGeneratedCounterCell

Equations

• instDecidableEqSortGeneratedCounterCell = decEqSortGeneratedCounterCell✝

structure SortNumberCell : Type

• val : SortInt

instance instBEqSortNumberCell : BEq SortNumberCell

Equations

• instBEqSortNumberCell = { beq := beqSortNumberCell✝ }

instance instDecidableEqSortNumberCell : DecidableEq SortNumberCell

Equations

• instDecidableEqSortNumberCell = decEqSortNumberCell✝

structure SortTxMaxFeeCell : Type

• val : SortInt

instance instBEqSortTxMaxFeeCell : BEq SortTxMaxFeeCell

Equations

• instBEqSortTxMaxFeeCell = { beq := beqSortTxMaxFeeCell✝ }

instance instDecidableEqSortTxMaxFeeCell : DecidableEq SortTxMaxFeeCell

Equations

• instDecidableEqSortTxMaxFeeCell = decEqSortTxMaxFeeCell✝

structure SortTxGasLimitCell : Type

• val : SortInt

instance instBEqSortTxGasLimitCell : BEq SortTxGasLimitCell

Equations

• instBEqSortTxGasLimitCell = { beq := beqSortTxGasLimitCell✝ }

instance instDecidableEqSortTxGasLimitCell : DecidableEq SortTxGasLimitCell

Equations

• instDecidableEqSortTxGasLimitCell = decEqSortTxGasLimitCell✝

inductive SortGas : Type

• inj_SortInt (x : SortInt) : SortGas

instance instBEqSortGas : BEq SortGas

Equations

• instBEqSortGas = { beq := beqSortGas✝ }

instance instDecidableEqSortGas : DecidableEq SortGas

Equations

• instDecidableEqSortGas = decEqSortGas✝

structure SortExcessBlobGasCell : Type

• val : SortInt

instance instBEqSortExcessBlobGasCell : BEq SortExcessBlobGasCell

Equations

• instBEqSortExcessBlobGasCell = { beq := beqSortExcessBlobGasCell✝ }

instance instDecidableEqSortExcessBlobGasCell : DecidableEq SortExcessBlobGasCell

Equations

• instDecidableEqSortExcessBlobGasCell = decEqSortExcessBlobGasCell✝

structure SortTxNonceCell : Type

• val : SortInt

instance instBEqSortTxNonceCell : BEq SortTxNonceCell

Equations

• instBEqSortTxNonceCell = { beq := beqSortTxNonceCell✝ }

instance instDecidableEqSortTxNonceCell : DecidableEq SortTxNonceCell

Equations

• instDecidableEqSortTxNonceCell = decEqSortTxNonceCell✝

structure SortPcCell : Type

• val : SortInt

instance instBEqSortPcCell : BEq SortPcCell

Equations

• instBEqSortPcCell = { beq := beqSortPcCell✝ }

instance instDecidableEqSortPcCell : DecidableEq SortPcCell

Equations

• instDecidableEqSortPcCell = decEqSortPcCell✝

structure SortAmountCell : Type

• val : SortInt

instance instBEqSortAmountCell : BEq SortAmountCell

Equations

• instBEqSortAmountCell = { beq := beqSortAmountCell✝ }

instance instDecidableEqSortAmountCell : DecidableEq SortAmountCell

Equations

• instDecidableEqSortAmountCell = decEqSortAmountCell✝

structure SortGasLimitCell : Type

• val : SortInt

instance instBEqSortGasLimitCell : BEq SortGasLimitCell

Equations

• instBEqSortGasLimitCell = { beq := beqSortGasLimitCell✝ }

instance instDecidableEqSortGasLimitCell : DecidableEq SortGasLimitCell

Equations

• instDecidableEqSortGasLimitCell = decEqSortGasLimitCell✝

structure SortTxGasPriceCell : Type

• val : SortInt

instance instBEqSortTxGasPriceCell : BEq SortTxGasPriceCell

Equations

• instBEqSortTxGasPriceCell = { beq := beqSortTxGasPriceCell✝ }

instance instDecidableEqSortTxGasPriceCell : DecidableEq SortTxGasPriceCell

Equations

• instDecidableEqSortTxGasPriceCell = decEqSortTxGasPriceCell✝

structure SortGasPriceCell : Type

• val : SortInt

instance instBEqSortGasPriceCell : BEq SortGasPriceCell

Equations

• instBEqSortGasPriceCell = { beq := beqSortGasPriceCell✝ }

instance instDecidableEqSortGasPriceCell : DecidableEq SortGasPriceCell

Equations

• instDecidableEqSortGasPriceCell = decEqSortGasPriceCell✝

structure SortMemoryUsedCell : Type

• val : SortInt

instance instBEqSortMemoryUsedCell : BEq SortMemoryUsedCell

Equations

• instBEqSortMemoryUsedCell = { beq := beqSortMemoryUsedCell✝ }

instance instDecidableEqSortMemoryUsedCell : DecidableEq SortMemoryUsedCell

Equations

• instDecidableEqSortMemoryUsedCell = decEqSortMemoryUsedCell✝

structure SortMsgIDCell : Type

• val : SortInt

instance instBEqSortMsgIDCell : BEq SortMsgIDCell

Equations

• instBEqSortMsgIDCell = { beq := beqSortMsgIDCell✝ }

instance instDecidableEqSortMsgIDCell : DecidableEq SortMsgIDCell

Equations

• instDecidableEqSortMsgIDCell = decEqSortMsgIDCell✝

structure SortWithdrawalIDCell : Type

• val : SortInt

instance instBEqSortWithdrawalIDCell : BEq SortWithdrawalIDCell

Equations

• instBEqSortWithdrawalIDCell = { beq := beqSortWithdrawalIDCell✝ }

instance instDecidableEqSortWithdrawalIDCell : DecidableEq SortWithdrawalIDCell

Equations

• instDecidableEqSortWithdrawalIDCell = decEqSortWithdrawalIDCell✝

structure SortBeaconRootCell : Type

• val : SortInt

instance instBEqSortBeaconRootCell : BEq SortBeaconRootCell

Equations

• instBEqSortBeaconRootCell = { beq := beqSortBeaconRootCell✝ }

instance instDecidableEqSortBeaconRootCell : DecidableEq SortBeaconRootCell

Equations

• instDecidableEqSortBeaconRootCell = decEqSortBeaconRootCell✝

structure SortBaseFeeCell : Type

• val : SortInt

instance instBEqSortBaseFeeCell : BEq SortBaseFeeCell

Equations

• instBEqSortBaseFeeCell = { beq := beqSortBaseFeeCell✝ }

instance instDecidableEqSortBaseFeeCell : DecidableEq SortBaseFeeCell

Equations

• instDecidableEqSortBaseFeeCell = decEqSortBaseFeeCell✝

inductive SortAccount : Type

• inj_SortInt (x : SortInt) : SortAccount
• «.Account_EVM-TYPES_Account» : SortAccount

instance instBEqSortAccount : BEq SortAccount

Equations

• instBEqSortAccount = { beq := beqSortAccount✝ }

instance instDecidableEqSortAccount : DecidableEq SortAccount

Equations

• instDecidableEqSortAccount = decEqSortAccount✝

structure SortIndexCell : Type

• val : SortInt

instance instBEqSortIndexCell : BEq SortIndexCell

Equations

• instBEqSortIndexCell = { beq := beqSortIndexCell✝ }

instance instDecidableEqSortIndexCell : DecidableEq SortIndexCell

Equations

• instDecidableEqSortIndexCell = decEqSortIndexCell✝

structure SortTransactionsRootCell : Type

• val : SortInt

instance instBEqSortTransactionsRootCell : BEq SortTransactionsRootCell

Equations

• instBEqSortTransactionsRootCell = { beq := beqSortTransactionsRootCell✝ }

instance instDecidableEqSortTransactionsRootCell : DecidableEq SortTransactionsRootCell

Equations

• instDecidableEqSortTransactionsRootCell = decEqSortTransactionsRootCell✝

structure SortOmmersHashCell : Type

• val : SortInt

instance instBEqSortOmmersHashCell : BEq SortOmmersHashCell

Equations

• instBEqSortOmmersHashCell = { beq := beqSortOmmersHashCell✝ }

instance instDecidableEqSortOmmersHashCell : DecidableEq SortOmmersHashCell

Equations

• instDecidableEqSortOmmersHashCell = decEqSortOmmersHashCell✝

structure SortMixHashCell : Type

• val : SortInt

instance instBEqSortMixHashCell : BEq SortMixHashCell

Equations

• instBEqSortMixHashCell = { beq := beqSortMixHashCell✝ }

instance instDecidableEqSortMixHashCell : DecidableEq SortMixHashCell

Equations

• instDecidableEqSortMixHashCell = decEqSortMixHashCell✝

structure SortCallValueCell : Type

• val : SortInt

instance instBEqSortCallValueCell : BEq SortCallValueCell

Equations

• instBEqSortCallValueCell = { beq := beqSortCallValueCell✝ }

instance instDecidableEqSortCallValueCell : DecidableEq SortCallValueCell

Equations

• instDecidableEqSortCallValueCell = decEqSortCallValueCell✝

structure SortNonceCell : Type

• val : SortInt

instance instBEqSortNonceCell : BEq SortNonceCell

Equations

• instBEqSortNonceCell = { beq := beqSortNonceCell✝ }

instance instDecidableEqSortNonceCell : DecidableEq SortNonceCell

Equations

• instDecidableEqSortNonceCell = decEqSortNonceCell✝

structure SortWithdrawalsRootCell : Type

• val : SortInt

instance instBEqSortWithdrawalsRootCell : BEq SortWithdrawalsRootCell

Equations

• instBEqSortWithdrawalsRootCell = { beq := beqSortWithdrawalsRootCell✝ }

instance instDecidableEqSortWithdrawalsRootCell : DecidableEq SortWithdrawalsRootCell

Equations

• instDecidableEqSortWithdrawalsRootCell = decEqSortWithdrawalsRootCell✝

structure SortStateRootCell : Type

• val : SortInt

instance instBEqSortStateRootCell : BEq SortStateRootCell

Equations

• instBEqSortStateRootCell = { beq := beqSortStateRootCell✝ }

instance instDecidableEqSortStateRootCell : DecidableEq SortStateRootCell

Equations

• instDecidableEqSortStateRootCell = decEqSortStateRootCell✝

structure SortSigVCell : Type

• val : SortInt

instance instBEqSortSigVCell : BEq SortSigVCell

Equations

• instBEqSortSigVCell = { beq := beqSortSigVCell✝ }

instance instDecidableEqSortSigVCell : DecidableEq SortSigVCell

Equations

• instDecidableEqSortSigVCell = decEqSortSigVCell✝

structure SortExitCodeCell : Type

• val : SortInt

instance instBEqSortExitCodeCell : BEq SortExitCodeCell

Equations

• instBEqSortExitCodeCell = { beq := beqSortExitCodeCell✝ }

instance instDecidableEqSortExitCodeCell : DecidableEq SortExitCodeCell

Equations

• instDecidableEqSortExitCodeCell = decEqSortExitCodeCell✝

structure SortValidatorIndexCell : Type

• val : SortInt

instance instBEqSortValidatorIndexCell : BEq SortValidatorIndexCell

Equations

• instBEqSortValidatorIndexCell = { beq := beqSortValidatorIndexCell✝ }

instance instDecidableEqSortValidatorIndexCell : DecidableEq SortValidatorIndexCell

Equations

• instDecidableEqSortValidatorIndexCell = decEqSortValidatorIndexCell✝

structure SortTxMaxBlobFeeCell : Type

• val : SortInt

instance instBEqSortTxMaxBlobFeeCell : BEq SortTxMaxBlobFeeCell

Equations

• instBEqSortTxMaxBlobFeeCell = { beq := beqSortTxMaxBlobFeeCell✝ }

instance instDecidableEqSortTxMaxBlobFeeCell : DecidableEq SortTxMaxBlobFeeCell

Equations

• instDecidableEqSortTxMaxBlobFeeCell = decEqSortTxMaxBlobFeeCell✝

structure SortReceiptsRootCell : Type

• val : SortInt

instance instBEqSortReceiptsRootCell : BEq SortReceiptsRootCell

Equations

• instBEqSortReceiptsRootCell = { beq := beqSortReceiptsRootCell✝ }

instance instDecidableEqSortReceiptsRootCell : DecidableEq SortReceiptsRootCell

Equations

• instDecidableEqSortReceiptsRootCell = decEqSortReceiptsRootCell✝

structure SortTxPriorityFeeCell : Type

• val : SortInt

instance instBEqSortTxPriorityFeeCell : BEq SortTxPriorityFeeCell

Equations

• instBEqSortTxPriorityFeeCell = { beq := beqSortTxPriorityFeeCell✝ }

instance instDecidableEqSortTxPriorityFeeCell : DecidableEq SortTxPriorityFeeCell

Equations

• instDecidableEqSortTxPriorityFeeCell = decEqSortTxPriorityFeeCell✝

structure SortDifficultyCell : Type

• val : SortInt

instance instBEqSortDifficultyCell : BEq SortDifficultyCell

Equations

• instBEqSortDifficultyCell = { beq := beqSortDifficultyCell✝ }

instance instDecidableEqSortDifficultyCell : DecidableEq SortDifficultyCell

Equations

• instDecidableEqSortDifficultyCell = decEqSortDifficultyCell✝

structure SortChainIDCell : Type

• val : SortInt

instance instBEqSortChainIDCell : BEq SortChainIDCell

Equations

• instBEqSortChainIDCell = { beq := beqSortChainIDCell✝ }

instance instDecidableEqSortChainIDCell : DecidableEq SortChainIDCell

Equations

• instDecidableEqSortChainIDCell = decEqSortChainIDCell✝

inductive SortAccountCode : Type

• inj_SortBytes (x : SortBytes) : SortAccountCode

instance instBEqSortAccountCode : BEq SortAccountCode

Equations

• instBEqSortAccountCode = { beq := beqSortAccountCode✝ }

instance instDecidableEqSortAccountCode : DecidableEq SortAccountCode

Equations

• instDecidableEqSortAccountCode = decEqSortAccountCode✝

structure SortExtraDataCell : Type

• val : SortBytes

instance instBEqSortExtraDataCell : BEq SortExtraDataCell

Equations

• instBEqSortExtraDataCell = { beq := beqSortExtraDataCell✝ }

instance instDecidableEqSortExtraDataCell : DecidableEq SortExtraDataCell

Equations

• instDecidableEqSortExtraDataCell = decEqSortExtraDataCell✝

structure SortProgramCell : Type

• val : SortBytes

instance instBEqSortProgramCell : BEq SortProgramCell

Equations

• instBEqSortProgramCell = { beq := beqSortProgramCell✝ }

instance instDecidableEqSortProgramCell : DecidableEq SortProgramCell

Equations

• instDecidableEqSortProgramCell = decEqSortProgramCell✝

structure SortJumpDestsCell : Type

• val : SortBytes

instance instBEqSortJumpDestsCell : BEq SortJumpDestsCell

Equations

• instBEqSortJumpDestsCell = { beq := beqSortJumpDestsCell✝ }

instance instDecidableEqSortJumpDestsCell : DecidableEq SortJumpDestsCell

Equations

• instDecidableEqSortJumpDestsCell = decEqSortJumpDestsCell✝

structure SortSigSCell : Type

• val : SortBytes

instance instBEqSortSigSCell : BEq SortSigSCell

Equations

• instBEqSortSigSCell = { beq := beqSortSigSCell✝ }

instance instDecidableEqSortSigSCell : DecidableEq SortSigSCell

Equations

• instDecidableEqSortSigSCell = decEqSortSigSCell✝

structure SortOutputCell : Type

• val : SortBytes

instance instBEqSortOutputCell : BEq SortOutputCell

Equations

• instBEqSortOutputCell = { beq := beqSortOutputCell✝ }

instance instDecidableEqSortOutputCell : DecidableEq SortOutputCell

Equations

• instDecidableEqSortOutputCell = decEqSortOutputCell✝

structure SortDataCell : Type

• val : SortBytes

instance instBEqSortDataCell : BEq SortDataCell

Equations

• instBEqSortDataCell = { beq := beqSortDataCell✝ }

instance instDecidableEqSortDataCell : DecidableEq SortDataCell

Equations

• instDecidableEqSortDataCell = decEqSortDataCell✝

structure SortCallDataCell : Type

• val : SortBytes

instance instBEqSortCallDataCell : BEq SortCallDataCell

Equations

• instBEqSortCallDataCell = { beq := beqSortCallDataCell✝ }

instance instDecidableEqSortCallDataCell : DecidableEq SortCallDataCell

Equations

• instDecidableEqSortCallDataCell = decEqSortCallDataCell✝

structure SortSigRCell : Type

• val : SortBytes

instance instBEqSortSigRCell : BEq SortSigRCell

Equations

• instBEqSortSigRCell = { beq := beqSortSigRCell✝ }

instance instDecidableEqSortSigRCell : DecidableEq SortSigRCell

Equations

• instDecidableEqSortSigRCell = decEqSortSigRCell✝

structure SortLocalMemCell : Type

• val : SortBytes

instance instBEqSortLocalMemCell : BEq SortLocalMemCell

Equations

• instBEqSortLocalMemCell = { beq := beqSortLocalMemCell✝ }

instance instDecidableEqSortLocalMemCell : DecidableEq SortLocalMemCell

Equations

• instDecidableEqSortLocalMemCell = decEqSortLocalMemCell✝

structure SortLogsBloomCell : Type

• val : SortBytes

instance instBEqSortLogsBloomCell : BEq SortLogsBloomCell

Equations

• instBEqSortLogsBloomCell = { beq := beqSortLogsBloomCell✝ }

instance instDecidableEqSortLogsBloomCell : DecidableEq SortLogsBloomCell

Equations

• instDecidableEqSortLogsBloomCell = decEqSortLogsBloomCell✝

inductive SortInternalOp : Type

• #next[_]_EVM_InternalOp_MaybeOpCode (x0 : SortMaybeOpCode) : SortInternalOp

instance instBEqSortMaybeOpCode : BEq SortMaybeOpCode

Equations

• instBEqSortMaybeOpCode = { beq := beqSortMaybeOpCode✝ }

instance instBEqSortInternalOp : BEq SortInternalOp

Equations

• instBEqSortInternalOp = { beq := beqSortInternalOp✝ }

instance instDecidableEqSortMaybeOpCode : DecidableEq SortMaybeOpCode

Equations

• instDecidableEqSortMaybeOpCode = decEqSortMaybeOpCode✝

instance instDecidableEqSortInternalOp : DecidableEq SortInternalOp

Equations

• instDecidableEqSortInternalOp = decEqSortInternalOp✝

inductive SortMaybeOpCode : Type

• inj_SortBinStackOp (x : SortBinStackOp) : SortMaybeOpCode
• inj_SortInternalOp (x : SortInternalOp) : SortMaybeOpCode
• inj_SortNullStackOp (x : SortNullStackOp) : SortMaybeOpCode
• inj_SortPushOp (x : SortPushOp) : SortMaybeOpCode
• inj_SortTernStackOp (x : SortTernStackOp) : SortMaybeOpCode
• inj_SortUnStackOp (x : SortUnStackOp) : SortMaybeOpCode

structure SortStaticCell : Type

• val : SortBool

instance instBEqSortStaticCell : BEq SortStaticCell

Equations

• instBEqSortStaticCell = { beq := beqSortStaticCell✝ }

instance instDecidableEqSortStaticCell : DecidableEq SortStaticCell

Equations

• instDecidableEqSortStaticCell = decEqSortStaticCell✝

structure SortUseGasCell : Type

• val : SortBool

instance instBEqSortUseGasCell : BEq SortUseGasCell

Equations

• instBEqSortUseGasCell = { beq := beqSortUseGasCell✝ }

instance instDecidableEqSortUseGasCell : DecidableEq SortUseGasCell

Equations

• instDecidableEqSortUseGasCell = decEqSortUseGasCell✝

structure SortModeCell : Type

• val : SortMode

instance instBEqSortModeCell : BEq SortModeCell

Equations

• instBEqSortModeCell = { beq := beqSortModeCell✝ }

instance instDecidableEqSortModeCell : DecidableEq SortModeCell

Equations

• instDecidableEqSortModeCell = decEqSortModeCell✝

structure SortWordStackCell : Type

• val : SortWordStack

instance instBEqSortWordStackCell : BEq SortWordStackCell

Equations

• instBEqSortWordStackCell = { beq := beqSortWordStackCell✝ }

instance instDecidableEqSortWordStackCell : DecidableEq SortWordStackCell

Equations

• instDecidableEqSortWordStackCell = decEqSortWordStackCell✝

structure SortGasCell : Type

• val : SortGas

instance instBEqSortGasCell : BEq SortGasCell

Equations

• instBEqSortGasCell = { beq := beqSortGasCell✝ }

instance instDecidableEqSortGasCell : DecidableEq SortGasCell

Equations

• instDecidableEqSortGasCell = decEqSortGasCell✝

structure SortCallGasCell : Type

• val : SortGas

instance instBEqSortCallGasCell : BEq SortCallGasCell

Equations

• instBEqSortCallGasCell = { beq := beqSortCallGasCell✝ }

instance instDecidableEqSortCallGasCell : DecidableEq SortCallGasCell

Equations

• instDecidableEqSortCallGasCell = decEqSortCallGasCell✝

structure SortGasUsedCell : Type

• val : SortGas

instance instBEqSortGasUsedCell : BEq SortGasUsedCell

Equations

• instBEqSortGasUsedCell = { beq := beqSortGasUsedCell✝ }

instance instDecidableEqSortGasUsedCell : DecidableEq SortGasUsedCell

Equations

• instDecidableEqSortGasUsedCell = decEqSortGasUsedCell✝

structure SortIdCell : Type

• val : SortAccount

instance instBEqSortIdCell : BEq SortIdCell

Equations

• instBEqSortIdCell = { beq := beqSortIdCell✝ }

instance instDecidableEqSortIdCell : DecidableEq SortIdCell

Equations

• instDecidableEqSortIdCell = decEqSortIdCell✝

structure SortToCell : Type

• val : SortAccount

instance instBEqSortToCell : BEq SortToCell

Equations

• instBEqSortToCell = { beq := beqSortToCell✝ }

instance instDecidableEqSortToCell : DecidableEq SortToCell

Equations

• instDecidableEqSortToCell = decEqSortToCell✝

structure SortAddressCell : Type

• val : SortAccount

instance instBEqSortAddressCell : BEq SortAddressCell

Equations

• instBEqSortAddressCell = { beq := beqSortAddressCell✝ }

instance instDecidableEqSortAddressCell : DecidableEq SortAddressCell

Equations

• instDecidableEqSortAddressCell = decEqSortAddressCell✝

structure SortOriginCell : Type

• val : SortAccount

instance instBEqSortOriginCell : BEq SortOriginCell

Equations

• instBEqSortOriginCell = { beq := beqSortOriginCell✝ }

instance instDecidableEqSortOriginCell : DecidableEq SortOriginCell

Equations

• instDecidableEqSortOriginCell = decEqSortOriginCell✝

structure SortCallerCell : Type

• val : SortAccount

instance instBEqSortCallerCell : BEq SortCallerCell

Equations

• instBEqSortCallerCell = { beq := beqSortCallerCell✝ }

instance instDecidableEqSortCallerCell : DecidableEq SortCallerCell

Equations

• instDecidableEqSortCallerCell = decEqSortCallerCell✝

structure SortCodeCell : Type

• val : SortAccountCode

instance instBEqSortCodeCell : BEq SortCodeCell

Equations

• instBEqSortCodeCell = { beq := beqSortCodeCell✝ }

instance instDecidableEqSortCodeCell : DecidableEq SortCodeCell

Equations

• instDecidableEqSortCodeCell = decEqSortCodeCell✝

structure SortWithdrawalCell : Type

• withdrawalID : SortWithdrawalIDCell
• index : SortIndexCell
• validatorIndex : SortValidatorIndexCell
• address : SortAddressCell
• amount : SortAmountCell

instance instBEqSortWithdrawalCell : BEq SortWithdrawalCell

Equations

• instBEqSortWithdrawalCell = { beq := beqSortWithdrawalCell✝ }

instance instDecidableEqSortWithdrawalCell : DecidableEq SortWithdrawalCell

Equations

• instDecidableEqSortWithdrawalCell = decEqSortWithdrawalCell✝

structure SortCallStateCell : Type

• program : SortProgramCell
• jumpDests : SortJumpDestsCell
• id : SortIdCell
• caller : SortCallerCell
• callData : SortCallDataCell
• callValue : SortCallValueCell
• wordStack : SortWordStackCell
• localMem : SortLocalMemCell
• pc : SortPcCell
• gas : SortGasCell
• memoryUsed : SortMemoryUsedCell
• callGas : SortCallGasCell
• static : SortStaticCell
• callDepth : SortCallDepthCell

instance instBEqSortCallStateCell : BEq SortCallStateCell

Equations

• instBEqSortCallStateCell = { beq := beqSortCallStateCell✝ }

instance instDecidableEqSortCallStateCell : DecidableEq SortCallStateCell

Equations

• instDecidableEqSortCallStateCell = decEqSortCallStateCell✝

structure SortWithdrawalCellMap : Type

• coll : List (SortWithdrawalIDCell × SortWithdrawalCell)

instance instBEqSortWithdrawalCellMap : BEq SortWithdrawalCellMap

Equations

• instBEqSortWithdrawalCellMap = { beq := beqSortWithdrawalCellMap✝ }

instance instDecidableEqSortWithdrawalCellMap : DecidableEq SortWithdrawalCellMap

Equations

• instDecidableEqSortWithdrawalCellMap = decEqSortWithdrawalCellMap✝

structure SortWithdrawalsCell : Type

• val : SortWithdrawalCellMap

instance instBEqSortWithdrawalsCell : BEq SortWithdrawalsCell

Equations

• instBEqSortWithdrawalsCell = { beq := beqSortWithdrawalsCell✝ }

instance instDecidableEqSortWithdrawalsCell : DecidableEq SortWithdrawalsCell

Equations

• instDecidableEqSortWithdrawalsCell = decEqSortWithdrawalsCell✝

structure SortAccessedAccountsCell : Type

• val : SortSet

instance instBEqSortWithdrawalsPendingCell : BEq SortWithdrawalsPendingCell

Equations

• instBEqSortWithdrawalsPendingCell = { beq := beqSortWithdrawalsPendingCell✝ }

instance instBEqSortBlockhashesCell : BEq SortBlockhashesCell

Equations

• instBEqSortBlockhashesCell = { beq := beqSortBlockhashesCell✝ }

instance instBEqSortSelfDestructCell : BEq SortSelfDestructCell

Equations

• instBEqSortSelfDestructCell = { beq := beqSortSelfDestructCell✝ }

instance instBEqSortCreatedAccountsCell : BEq SortCreatedAccountsCell

Equations

• instBEqSortCreatedAccountsCell = { beq := beqSortCreatedAccountsCell✝ }

instance instBEqSortList : BEq SortList

Equations

• instBEqSortList = { beq := beqSortList✝ }

instance instBEqSortMessagesCell : BEq SortMessagesCell

Equations

• instBEqSortMessagesCell = { beq := beqSortMessagesCell✝ }

instance instBEqSortJSON : BEq SortJSON

Equations

• instBEqSortJSON = { beq := beqSortJSON✝ }

instance instBEqSortSubstateCell : BEq SortSubstateCell

Equations

• instBEqSortSubstateCell = { beq := beqSortSubstateCell✝ }

instance instBEqSortTxPendingCell : BEq SortTxPendingCell

Equations

• instBEqSortTxPendingCell = { beq := beqSortTxPendingCell✝ }

instance instBEqSortKCell : BEq SortKCell

Equations

• instBEqSortKCell = { beq := beqSortKCell✝ }

instance instBEqSortMessageCellMap : BEq SortMessageCellMap

Equations

• instBEqSortMessageCellMap = { beq := beqSortMessageCellMap✝ }

instance instBEqSortGeneratedTopCell : BEq SortGeneratedTopCell

Equations

• instBEqSortGeneratedTopCell = { beq := beqSortGeneratedTopCell✝ }

instance instBEqSortMessageCell : BEq SortMessageCell

Equations

• instBEqSortMessageCell = { beq := beqSortMessageCell✝ }

instance instBEqSortCallStackCell : BEq SortCallStackCell

Equations

• instBEqSortCallStackCell = { beq := beqSortCallStackCell✝ }

instance instBEqSortAccessedAccountsCell : BEq SortAccessedAccountsCell

Equations

• instBEqSortAccessedAccountsCell = { beq := beqSortAccessedAccountsCell✝ }

instance instBEqSortNetworkCell : BEq SortNetworkCell

Equations

• instBEqSortNetworkCell = { beq := beqSortNetworkCell✝ }

instance instBEqSortOrigStorageCell : BEq SortOrigStorageCell

Equations

• instBEqSortOrigStorageCell = { beq := beqSortOrigStorageCell✝ }

instance instBEqSortTransientStorageCell : BEq SortTransientStorageCell

Equations

• instBEqSortTransientStorageCell = { beq := beqSortTransientStorageCell✝ }

instance instBEqSortKItem : BEq SortKItem

Equations

• instBEqSortKItem = { beq := beqSortKItem✝ }

instance instBEqSortAccountCell : BEq SortAccountCell

Equations

• instBEqSortAccountCell = { beq := beqSortAccountCell✝ }

instance instBEqSortEvmCell : BEq SortEvmCell

Equations

• instBEqSortEvmCell = { beq := beqSortEvmCell✝ }

instance instBEqSortJSONs : BEq SortJSONs

Equations

• instBEqSortJSONs = { beq := beqSortJSONs✝ }

instance instBEqSortOmmerBlockHeadersCell : BEq SortOmmerBlockHeadersCell

Equations

• instBEqSortOmmerBlockHeadersCell = { beq := beqSortOmmerBlockHeadersCell✝ }

instance instBEqSortK : BEq SortK

Equations

• instBEqSortK = { beq := beqSortK✝ }

instance instBEqSortEthereumCell : BEq SortEthereumCell

Equations

• instBEqSortEthereumCell = { beq := beqSortEthereumCell✝ }

instance instBEqSortBlockCell : BEq SortBlockCell

Equations

• instBEqSortBlockCell = { beq := beqSortBlockCell✝ }

instance instBEqSortWithdrawalsOrderCell : BEq SortWithdrawalsOrderCell

Equations

• instBEqSortWithdrawalsOrderCell = { beq := beqSortWithdrawalsOrderCell✝ }

instance instBEqSortAccountsCell : BEq SortAccountsCell

Equations

• instBEqSortAccountsCell = { beq := beqSortAccountsCell✝ }

instance instBEqSortStorageCell : BEq SortStorageCell

Equations

• instBEqSortStorageCell = { beq := beqSortStorageCell✝ }

instance instBEqSortSet : BEq SortSet

Equations

• instBEqSortSet = { beq := beqSortSet✝ }

instance instBEqSortTxVersionedHashesCell : BEq SortTxVersionedHashesCell

Equations

• instBEqSortTxVersionedHashesCell = { beq := beqSortTxVersionedHashesCell✝ }

instance instBEqSortTxOrderCell : BEq SortTxOrderCell

Equations

• instBEqSortTxOrderCell = { beq := beqSortTxOrderCell✝ }

instance instBEqSortMap : BEq SortMap

Equations

• instBEqSortMap = { beq := beqSortMap✝ }

instance instBEqSortTxAccessCell : BEq SortTxAccessCell

Equations

• instBEqSortTxAccessCell = { beq := beqSortTxAccessCell✝ }

instance instBEqSortInterimStatesCell : BEq SortInterimStatesCell

Equations

• instBEqSortInterimStatesCell = { beq := beqSortInterimStatesCell✝ }

instance instBEqSortVersionedHashesCell : BEq SortVersionedHashesCell

Equations

• instBEqSortVersionedHashesCell = { beq := beqSortVersionedHashesCell✝ }

instance instBEqSortTouchedAccountsCell : BEq SortTouchedAccountsCell

Equations

• instBEqSortTouchedAccountsCell = { beq := beqSortTouchedAccountsCell✝ }

instance instBEqSortKevmCell : BEq SortKevmCell

Equations

• instBEqSortKevmCell = { beq := beqSortKevmCell✝ }

instance instBEqSortAccessedStorageCell : BEq SortAccessedStorageCell

Equations

• instBEqSortAccessedStorageCell = { beq := beqSortAccessedStorageCell✝ }

instance instBEqSortLogCell : BEq SortLogCell

Equations

• instBEqSortLogCell = { beq := beqSortLogCell✝ }

instance instBEqSortAccountCellMap : BEq SortAccountCellMap

Equations

• instBEqSortAccountCellMap = { beq := beqSortAccountCellMap✝ }

structure SortAccessedStorageCell : Type

• val : SortMap

structure SortAccountCell : Type

• acctID : SortAcctIDCell
• balance : SortBalanceCell
• code : SortCodeCell
• storage : SortStorageCell
• origStorage : SortOrigStorageCell
• transientStorage : SortTransientStorageCell
• nonce : SortNonceCell

structure SortAccountCellMap : Type

• coll : List (SortAcctIDCell × SortAccountCell)

structure SortAccountsCell : Type

• val : SortAccountCellMap

structure SortBlockCell : Type

• previousHash : SortPreviousHashCell
• ommersHash : SortOmmersHashCell
• coinbase : SortCoinbaseCell
• stateRoot : SortStateRootCell
• transactionsRoot : SortTransactionsRootCell
• receiptsRoot : SortReceiptsRootCell
• logsBloom : SortLogsBloomCell
• difficulty : SortDifficultyCell
• number : SortNumberCell
• gasLimit : SortGasLimitCell
• gasUsed : SortGasUsedCell
• timestamp : SortTimestampCell
• extraData : SortExtraDataCell
• mixHash : SortMixHashCell
• blockNonce : SortBlockNonceCell
• baseFee : SortBaseFeeCell
• withdrawalsRoot : SortWithdrawalsRootCell
• blobGasUsed : SortBlobGasUsedCell
• excessBlobGas : SortExcessBlobGasCell
• beaconRoot : SortBeaconRootCell
• ommerBlockHeaders : SortOmmerBlockHeadersCell

structure SortBlockhashesCell : Type

• val : SortList

structure SortCallStackCell : Type

• val : SortList

structure SortCreatedAccountsCell : Type

• val : SortSet

structure SortEthereumCell : Type

• evm : SortEvmCell
• network : SortNetworkCell

structure SortEvmCell : Type

• output : SortOutputCell
• statusCode : SortStatusCodeCell
• callStack : SortCallStackCell
• interimStates : SortInterimStatesCell
• touchedAccounts : SortTouchedAccountsCell
• callState : SortCallStateCell
• versionedHashes : SortVersionedHashesCell
• substate : SortSubstateCell
• gasPrice : SortGasPriceCell
• origin : SortOriginCell
• blockhashes : SortBlockhashesCell
• block : SortBlockCell

structure SortGeneratedTopCell : Type

• kevm : SortKevmCell
• generatedCounter : SortGeneratedCounterCell

structure SortInterimStatesCell : Type

• val : SortList

inductive SortJSON : Type

• inj_SortAccount (x : SortAccount) : SortJSON
• inj_SortBool (x : SortBool) : SortJSON
• inj_SortBytes (x : SortBytes) : SortJSON
• inj_SortInt (x : SortInt) : SortJSON
• inj_SortMap (x : SortMap) : SortJSON
• inj_SortTxType (x : SortTxType) : SortJSON
• JSONEntry (x0 : SortJSONKey) (x1 : SortJSON) : SortJSON
• JSONList (x0 : SortJSONs) : SortJSON
• JSONObject (x0 : SortJSONs) : SortJSON
• JSONnull : SortJSON

inductive SortJSONs : Type

• «.List{"JSONs"}» : SortJSONs
• JSONs (x0 : SortJSON) (x1 : SortJSONs) : SortJSONs

inductive SortK : Type

• dotk : SortK
• kseq (x0 : SortKItem) (x1 : SortK) : SortK

structure SortKCell : Type

• val : SortK

inductive SortKItem : Type

• inj_SortAccessedAccountsCell (x : SortAccessedAccountsCell) : SortKItem
• inj_SortAccessedStorageCell (x : SortAccessedStorageCell) : SortKItem
• inj_SortAccount (x : SortAccount) : SortKItem
• inj_SortAccountCell (x : SortAccountCell) : SortKItem
• inj_SortAccountCellMap (x : SortAccountCellMap) : SortKItem
• inj_SortAccountCode (x : SortAccountCode) : SortKItem
• inj_SortAccountsCell (x : SortAccountsCell) : SortKItem
• inj_SortAcctIDCell (x : SortAcctIDCell) : SortKItem
• inj_SortAddressCell (x : SortAddressCell) : SortKItem
• inj_SortAmountCell (x : SortAmountCell) : SortKItem
• inj_SortBalanceCell (x : SortBalanceCell) : SortKItem
• inj_SortBaseFeeCell (x : SortBaseFeeCell) : SortKItem
• inj_SortBeaconRootCell (x : SortBeaconRootCell) : SortKItem
• inj_SortBinStackOp (x : SortBinStackOp) : SortKItem
• inj_SortBlobGasUsedCell (x : SortBlobGasUsedCell) : SortKItem
• inj_SortBlockCell (x : SortBlockCell) : SortKItem
• inj_SortBlockNonceCell (x : SortBlockNonceCell) : SortKItem
• inj_SortBlockhashesCell (x : SortBlockhashesCell) : SortKItem
• inj_SortBool (x : SortBool) : SortKItem
• inj_SortBytes (x : SortBytes) : SortKItem
• inj_SortCallDataCell (x : SortCallDataCell) : SortKItem
• inj_SortCallDepthCell (x : SortCallDepthCell) : SortKItem
• inj_SortCallGasCell (x : SortCallGasCell) : SortKItem
• inj_SortCallStackCell (x : SortCallStackCell) : SortKItem
• inj_SortCallStateCell (x : SortCallStateCell) : SortKItem
• inj_SortCallValueCell (x : SortCallValueCell) : SortKItem
• inj_SortCallerCell (x : SortCallerCell) : SortKItem
• inj_SortChainIDCell (x : SortChainIDCell) : SortKItem
• inj_SortCodeCell (x : SortCodeCell) : SortKItem
• inj_SortCoinbaseCell (x : SortCoinbaseCell) : SortKItem
• inj_SortCreatedAccountsCell (x : SortCreatedAccountsCell) : SortKItem
• inj_SortDataCell (x : SortDataCell) : SortKItem
• inj_SortDifficultyCell (x : SortDifficultyCell) : SortKItem
• inj_SortEndianness (x : SortEndianness) : SortKItem
• inj_SortEthereumCell (x : SortEthereumCell) : SortKItem
• inj_SortEvmCell (x : SortEvmCell) : SortKItem
• inj_SortExcessBlobGasCell (x : SortExcessBlobGasCell) : SortKItem
• inj_SortExitCodeCell (x : SortExitCodeCell) : SortKItem
• inj_SortExtraDataCell (x : SortExtraDataCell) : SortKItem
• inj_SortGas (x : SortGas) : SortKItem
• inj_SortGasCell (x : SortGasCell) : SortKItem
• inj_SortGasLimitCell (x : SortGasLimitCell) : SortKItem
• inj_SortGasPriceCell (x : SortGasPriceCell) : SortKItem
• inj_SortGasUsedCell (x : SortGasUsedCell) : SortKItem
• inj_SortGeneratedCounterCell (x : SortGeneratedCounterCell) : SortKItem
• inj_SortGeneratedTopCell (x : SortGeneratedTopCell) : SortKItem
• inj_SortIdCell (x : SortIdCell) : SortKItem
• inj_SortIndexCell (x : SortIndexCell) : SortKItem
• inj_SortInt (x : SortInt) : SortKItem
• inj_SortInterimStatesCell (x : SortInterimStatesCell) : SortKItem
• inj_SortInternalOp (x : SortInternalOp) : SortKItem
• inj_SortJSON (x : SortJSON) : SortKItem
• inj_SortJSONKey (x : SortJSONKey) : SortKItem
• inj_SortJSONs (x : SortJSONs) : SortKItem
• inj_SortJumpDestsCell (x : SortJumpDestsCell) : SortKItem
• inj_SortKCell (x : SortKCell) : SortKItem
• inj_SortKevmCell (x : SortKevmCell) : SortKItem
• inj_SortList (x : SortList) : SortKItem
• inj_SortLocalMemCell (x : SortLocalMemCell) : SortKItem
• inj_SortLogCell (x : SortLogCell) : SortKItem
• inj_SortLogsBloomCell (x : SortLogsBloomCell) : SortKItem
• inj_SortMap (x : SortMap) : SortKItem
• inj_SortMaybeOpCode (x : SortMaybeOpCode) : SortKItem
• inj_SortMemoryUsedCell (x : SortMemoryUsedCell) : SortKItem
• inj_SortMessageCell (x : SortMessageCell) : SortKItem
• inj_SortMessageCellMap (x : SortMessageCellMap) : SortKItem
• inj_SortMessagesCell (x : SortMessagesCell) : SortKItem
• inj_SortMixHashCell (x : SortMixHashCell) : SortKItem
• inj_SortMode (x : SortMode) : SortKItem
• inj_SortModeCell (x : SortModeCell) : SortKItem
• inj_SortMsgIDCell (x : SortMsgIDCell) : SortKItem
• inj_SortNetworkCell (x : SortNetworkCell) : SortKItem
• inj_SortNonceCell (x : SortNonceCell) : SortKItem
• inj_SortNullStackOp (x : SortNullStackOp) : SortKItem
• inj_SortNumberCell (x : SortNumberCell) : SortKItem
• inj_SortOmmerBlockHeadersCell (x : SortOmmerBlockHeadersCell) : SortKItem
• inj_SortOmmersHashCell (x : SortOmmersHashCell) : SortKItem
• inj_SortOrigStorageCell (x : SortOrigStorageCell) : SortKItem
• inj_SortOriginCell (x : SortOriginCell) : SortKItem
• inj_SortOutputCell (x : SortOutputCell) : SortKItem
• inj_SortPcCell (x : SortPcCell) : SortKItem
• inj_SortPreviousHashCell (x : SortPreviousHashCell) : SortKItem
• inj_SortProgramCell (x : SortProgramCell) : SortKItem
• inj_SortPushOp (x : SortPushOp) : SortKItem
• inj_SortReceiptsRootCell (x : SortReceiptsRootCell) : SortKItem
• inj_SortRefundCell (x : SortRefundCell) : SortKItem
• inj_SortSchedule (x : SortSchedule) : SortKItem
• inj_SortScheduleCell (x : SortScheduleCell) : SortKItem
• inj_SortScheduleConst (x : SortScheduleConst) : SortKItem
• inj_SortScheduleFlag (x : SortScheduleFlag) : SortKItem
• inj_SortSelfDestructCell (x : SortSelfDestructCell) : SortKItem
• inj_SortSet (x : SortSet) : SortKItem
• inj_SortSigRCell (x : SortSigRCell) : SortKItem
• inj_SortSigSCell (x : SortSigSCell) : SortKItem
• inj_SortSigVCell (x : SortSigVCell) : SortKItem
• inj_SortSignedness (x : SortSignedness) : SortKItem
• inj_SortStateRootCell (x : SortStateRootCell) : SortKItem
• inj_SortStaticCell (x : SortStaticCell) : SortKItem
• inj_SortStatusCode (x : SortStatusCode) : SortKItem
• inj_SortStatusCodeCell (x : SortStatusCodeCell) : SortKItem
• inj_SortStorageCell (x : SortStorageCell) : SortKItem
• inj_SortSubstateCell (x : SortSubstateCell) : SortKItem
• inj_SortTernStackOp (x : SortTernStackOp) : SortKItem
• inj_SortTimestampCell (x : SortTimestampCell) : SortKItem
• inj_SortToCell (x : SortToCell) : SortKItem
• inj_SortTouchedAccountsCell (x : SortTouchedAccountsCell) : SortKItem
• inj_SortTransactionsRootCell (x : SortTransactionsRootCell) : SortKItem
• inj_SortTransientStorageCell (x : SortTransientStorageCell) : SortKItem
• inj_SortTxAccessCell (x : SortTxAccessCell) : SortKItem
• inj_SortTxChainIDCell (x : SortTxChainIDCell) : SortKItem
• inj_SortTxGasLimitCell (x : SortTxGasLimitCell) : SortKItem
• inj_SortTxGasPriceCell (x : SortTxGasPriceCell) : SortKItem
• inj_SortTxMaxBlobFeeCell (x : SortTxMaxBlobFeeCell) : SortKItem
• inj_SortTxMaxFeeCell (x : SortTxMaxFeeCell) : SortKItem
• inj_SortTxNonceCell (x : SortTxNonceCell) : SortKItem
• inj_SortTxOrderCell (x : SortTxOrderCell) : SortKItem
• inj_SortTxPendingCell (x : SortTxPendingCell) : SortKItem
• inj_SortTxPriorityFeeCell (x : SortTxPriorityFeeCell) : SortKItem
• inj_SortTxType (x : SortTxType) : SortKItem
• inj_SortTxTypeCell (x : SortTxTypeCell) : SortKItem
• inj_SortTxVersionedHashesCell (x : SortTxVersionedHashesCell) : SortKItem
• inj_SortUnStackOp (x : SortUnStackOp) : SortKItem
• inj_SortUseGasCell (x : SortUseGasCell) : SortKItem
• inj_SortValidatorIndexCell (x : SortValidatorIndexCell) : SortKItem
• inj_SortValueCell (x : SortValueCell) : SortKItem
• inj_SortVersionedHashesCell (x : SortVersionedHashesCell) : SortKItem
• inj_SortWithdrawalCell (x : SortWithdrawalCell) : SortKItem
• inj_SortWithdrawalCellMap (x : SortWithdrawalCellMap) : SortKItem
• inj_SortWithdrawalIDCell (x : SortWithdrawalIDCell) : SortKItem
• inj_SortWithdrawalsCell (x : SortWithdrawalsCell) : SortKItem
• inj_SortWithdrawalsOrderCell (x : SortWithdrawalsOrderCell) : SortKItem
• inj_SortWithdrawalsPendingCell (x : SortWithdrawalsPendingCell) : SortKItem
• inj_SortWithdrawalsRootCell (x : SortWithdrawalsRootCell) : SortKItem
• inj_SortWordStack (x : SortWordStack) : SortKItem
• inj_SortWordStackCell (x : SortWordStackCell) : SortKItem
• #accessAccounts__EVM_KItem_Account (x0 : SortAccount) : SortKItem
• #accessAccounts__EVM_KItem_Set (x0 : SortSet) : SortKItem
• #accessAccounts___EVM_KItem_Account_Account (x0 x1 : SortAccount) : SortKItem
• #accessAccounts____EVM_KItem_Account_Account_Set (x0 x1 : SortAccount) (x2 : SortSet) : SortKItem
• #accessStorage___EVM_KItem_Account_Int (x0 : SortAccount) (x1 : SortInt) : SortKItem
• #codeDeposit__EVM_KItem_Int (x0 : SortInt) : SortKItem
• #finishCodeDeposit___EVM_KItem_Int_Bytes (x0 : SortInt) (x1 : SortBytes) : SortKItem
• #freezerCcall1_ (x0 x1 x2 x3 x4 : SortK) : SortKItem
• #freezerCcallgas1_ (x0 x1 x2 x3 x4 : SortK) : SortKItem
• #freezerCselfdestruct1_ (x0 x1 : SortK) : SortKItem
• #initVM_EVM_KItem : SortKItem
• #mkCodeDeposit__EVM_KItem_Int (x0 : SortInt) : SortKItem
• #return___EVM_KItem_Int_Int (x0 x1 : SortInt) : SortKItem
• #touchAccounts__EVM_KItem_Account (x0 : SortAccount) : SortKItem
• #touchAccounts___EVM_KItem_Account_Account (x0 x1 : SortAccount) : SortKItem
• end (x0 : SortStatusCode) : SortKItem
• execute : SortKItem
• halt : SortKItem
• «loadCallState__STATE-UTILS_KItem_JSON» (x0 : SortJSON) : SortKItem
• loadProgram (x0 : SortBytes) : SortKItem

structure SortKevmCell : Type

• k : SortKCell
• exitCode : SortExitCodeCell
• mode : SortModeCell
• schedule : SortScheduleCell
• useGas : SortUseGasCell
• ethereum : SortEthereumCell

structure SortList : Type

• coll : List SortKItem

structure SortLogCell : Type

• val : SortList

structure SortMap : Type

• coll : List (SortKItem × SortKItem)

structure SortMessageCell : Type

• msgID : SortMsgIDCell
• txNonce : SortTxNonceCell
• txGasPrice : SortTxGasPriceCell
• txGasLimit : SortTxGasLimitCell
• to : SortToCell
• value : SortValueCell
• sigV : SortSigVCell
• sigR : SortSigRCell
• sigS : SortSigSCell
• data : SortDataCell
• txAccess : SortTxAccessCell
• txChainID : SortTxChainIDCell
• txPriorityFee : SortTxPriorityFeeCell
• txMaxFee : SortTxMaxFeeCell
• txType : SortTxTypeCell
• txMaxBlobFee : SortTxMaxBlobFeeCell
• txVersionedHashes : SortTxVersionedHashesCell

structure SortMessageCellMap : Type

• coll : List (SortMsgIDCell × SortMessageCell)

structure SortMessagesCell : Type

• val : SortMessageCellMap

structure SortNetworkCell : Type

• chainID : SortChainIDCell
• accounts : SortAccountsCell
• txOrder : SortTxOrderCell
• txPending : SortTxPendingCell
• messages : SortMessagesCell
• withdrawalsPending : SortWithdrawalsPendingCell
• withdrawalsOrder : SortWithdrawalsOrderCell
• withdrawals : SortWithdrawalsCell

structure SortOmmerBlockHeadersCell : Type

• val : SortJSON

structure SortOrigStorageCell : Type

• val : SortMap

structure SortSelfDestructCell : Type

• val : SortSet

structure SortSet : Type

• coll : List SortKItem

structure SortStorageCell : Type

• val : SortMap

structure SortSubstateCell : Type

• selfDestruct : SortSelfDestructCell
• log : SortLogCell
• refund : SortRefundCell
• accessedAccounts : SortAccessedAccountsCell
• accessedStorage : SortAccessedStorageCell
• createdAccounts : SortCreatedAccountsCell

structure SortTouchedAccountsCell : Type

• val : SortSet

structure SortTransientStorageCell : Type

• val : SortMap

structure SortTxAccessCell : Type

• val : SortJSON

structure SortTxOrderCell : Type

• val : SortList

structure SortTxPendingCell : Type

• val : SortList

structure SortTxVersionedHashesCell : Type

• val : SortList

structure SortVersionedHashesCell : Type

• val : SortList

structure SortWithdrawalsOrderCell : Type

• val : SortList

structure SortWithdrawalsPendingCell : Type

• val : SortList