@[instance_reducible]

instance UInt8.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt8

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance UInt8.instLeast? : Std.PRange.Least? UInt8

Equations

• UInt8.instLeast? = { least? := some 0 }

instance UInt8.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt8

theorem UInt8.succ?_ofBitVec {x : BitVec 8} : Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt8.succMany?_ofBitVec {k : Nat} {x : BitVec 8} : Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt8.upwardEnumerableLE_ofBitVec {x y : BitVec 8} : Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt8.upwardEnumerableLT_ofBitVec {x y : BitVec 8} : Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt8.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt8

instance UInt8.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt8

instance UInt8.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt8

@[instance_reducible]

instance UInt8.instHasSize : Std.Rxc.HasSize UInt8

Equations

• UInt8.instHasSize = { size := fun (lo hi : UInt8) => hi.toNat + 1 - lo.toNat }

theorem UInt8.rxcHasSize_eq_toBitVec {lo : BitVec 8} {hi : UInt8} : Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt8.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt8

instance UInt8.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt8

@[instance_reducible]

instance UInt8.instHasSize_1 : Std.Rxo.HasSize UInt8

Equations

• UInt8.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt8.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt8

instance UInt8.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt8

@[instance_reducible]

instance UInt8.instHasSize_2 : Std.Rxi.HasSize UInt8

Equations

• UInt8.instHasSize_2 = { size := fun (lo : UInt8) => 2 ^ 8 - lo.toNat }

theorem UInt8.rxiHasSize_eq_toBitVec {lo : BitVec 8} : Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt8.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt8

@[instance_reducible]

instance UInt16.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt16

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance UInt16.instLeast? : Std.PRange.Least? UInt16

Equations

• UInt16.instLeast? = { least? := some 0 }

instance UInt16.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt16

theorem UInt16.succ?_ofBitVec {x : BitVec 16} : Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt16.succMany?_ofBitVec {k : Nat} {x : BitVec 16} : Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt16.upwardEnumerableLE_ofBitVec {x y : BitVec 16} : Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt16.upwardEnumerableLT_ofBitVec {x y : BitVec 16} : Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt16.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt16

instance UInt16.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt16

instance UInt16.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt16

@[instance_reducible]

instance UInt16.instHasSize : Std.Rxc.HasSize UInt16

Equations

• UInt16.instHasSize = { size := fun (lo hi : UInt16) => hi.toNat + 1 - lo.toNat }

theorem UInt16.rxcHasSize_eq_toBitVec {lo : BitVec 16} {hi : UInt16} : Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt16.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt16

instance UInt16.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt16

@[instance_reducible]

instance UInt16.instHasSize_1 : Std.Rxo.HasSize UInt16

Equations

• UInt16.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt16.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt16

instance UInt16.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt16

@[instance_reducible]

instance UInt16.instHasSize_2 : Std.Rxi.HasSize UInt16

Equations

• UInt16.instHasSize_2 = { size := fun (lo : UInt16) => 2 ^ 16 - lo.toNat }

theorem UInt16.rxiHasSize_eq_toBitVec {lo : BitVec 16} : Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt16.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt16

@[instance_reducible]

instance UInt32.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt32

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance UInt32.instLeast? : Std.PRange.Least? UInt32

Equations

• UInt32.instLeast? = { least? := some 0 }

instance UInt32.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt32

theorem UInt32.succ?_ofBitVec {x : BitVec 32} : Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt32.succMany?_ofBitVec {k : Nat} {x : BitVec 32} : Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt32.upwardEnumerableLE_ofBitVec {x y : BitVec 32} : Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt32.upwardEnumerableLT_ofBitVec {x y : BitVec 32} : Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt32.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt32

instance UInt32.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt32

instance UInt32.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt32

@[instance_reducible]

instance UInt32.instHasSize : Std.Rxc.HasSize UInt32

Equations

• UInt32.instHasSize = { size := fun (lo hi : UInt32) => hi.toNat + 1 - lo.toNat }

theorem UInt32.rxcHasSize_eq_toBitVec {lo : BitVec 32} {hi : UInt32} : Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt32.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt32

instance UInt32.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt32

@[instance_reducible]

instance UInt32.instHasSize_1 : Std.Rxo.HasSize UInt32

Equations

• UInt32.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt32.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt32

instance UInt32.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt32

@[instance_reducible]

instance UInt32.instHasSize_2 : Std.Rxi.HasSize UInt32

Equations

• UInt32.instHasSize_2 = { size := fun (lo : UInt32) => 2 ^ 32 - lo.toNat }

theorem UInt32.rxiHasSize_eq_toBitVec {lo : BitVec 32} : Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt32.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt32

@[instance_reducible]

instance UInt64.instUpwardEnumerable : Std.PRange.UpwardEnumerable UInt64

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance UInt64.instLeast? : Std.PRange.Least? UInt64

Equations

• UInt64.instLeast? = { least? := some 0 }

instance UInt64.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? UInt64

theorem UInt64.succ?_ofBitVec {x : BitVec 64} : Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem UInt64.succMany?_ofBitVec {k : Nat} {x : BitVec 64} : Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem UInt64.upwardEnumerableLE_ofBitVec {x y : BitVec 64} : Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem UInt64.upwardEnumerableLT_ofBitVec {x y : BitVec 64} : Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance UInt64.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt64

instance UInt64.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt64

instance UInt64.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt64

@[instance_reducible]

instance UInt64.instHasSize : Std.Rxc.HasSize UInt64

Equations

• UInt64.instHasSize = { size := fun (lo hi : UInt64) => hi.toNat + 1 - lo.toNat }

theorem UInt64.rxcHasSize_eq_toBitVec {lo : BitVec 64} {hi : UInt64} : Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance UInt64.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt64

instance UInt64.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt64

@[instance_reducible]

instance UInt64.instHasSize_1 : Std.Rxo.HasSize UInt64

Equations

• UInt64.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance UInt64.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt64

instance UInt64.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite UInt64

@[instance_reducible]

instance UInt64.instHasSize_2 : Std.Rxi.HasSize UInt64

Equations

• UInt64.instHasSize_2 = { size := fun (lo : UInt64) => 2 ^ 64 - lo.toNat }

theorem UInt64.rxiHasSize_eq_toBitVec {lo : BitVec 64} : Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance UInt64.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt64

@[instance_reducible]

instance USize.instUpwardEnumerable : Std.PRange.UpwardEnumerable USize

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance USize.instLeast? : Std.PRange.Least? USize

Equations

• USize.instLeast? = { least? := some 0 }

instance USize.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? USize

theorem USize.succ?_ofBitVec {x : BitVec System.Platform.numBits} : Std.PRange.succ? { toBitVec := x } = ofBitVec <$> Std.PRange.succ? x

theorem USize.succMany?_ofBitVec {k : Nat} {x : BitVec System.Platform.numBits} : Std.PRange.succMany? k { toBitVec := x } = ofBitVec <$> Std.PRange.succMany? k x

theorem USize.upwardEnumerableLE_ofBitVec {x y : BitVec System.Platform.numBits} : Std.PRange.UpwardEnumerable.LE { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LE x y

theorem USize.upwardEnumerableLT_ofBitVec {x y : BitVec System.Platform.numBits} : Std.PRange.UpwardEnumerable.LT { toBitVec := x } { toBitVec := y } ↔ Std.PRange.UpwardEnumerable.LT x y

instance USize.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable USize

instance USize.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE USize

instance USize.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT USize

@[instance_reducible]

instance USize.instHasSize : Std.Rxc.HasSize USize

Equations

• USize.instHasSize = { size := fun (lo hi : USize) => hi.toNat + 1 - lo.toNat }

theorem USize.rxcHasSize_eq_toBitVec {lo : BitVec System.Platform.numBits} {hi : USize} : Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec

instance USize.instLawfulHasSize : Std.Rxc.LawfulHasSize USize

instance USize.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite USize

@[instance_reducible]

instance USize.instHasSize_1 : Std.Rxo.HasSize USize

Equations

• USize.instHasSize_1 = Std.Rxo.HasSize.ofClosed

instance USize.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize USize

instance USize.instIsAlwaysFinite_1 : Std.Rxo.IsAlwaysFinite USize

@[instance_reducible]

instance USize.instHasSize_2 : Std.Rxi.HasSize USize

Equations

• USize.instHasSize_2 = { size := fun (lo : USize) => 2 ^ System.Platform.numBits - lo.toNat }

theorem USize.rxiHasSize_eq_toBitVec {lo : BitVec System.Platform.numBits} : Std.Rxi.HasSize.size { toBitVec := lo } = Std.Rxi.HasSize.size lo

instance USize.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize USize