The following lemmas are stated purely in terms of BitVec n. Their assumptions and statements may seem technical, but they are exactly what is needed in the actual proofs.

instance Int8.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int8

Equations

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

instance Int8.instRxcHasSize : Std.Rxc.HasSize Int8

Equations

• Int8.instRxcHasSize = { size := fun (lo hi : Int8) => (hi.toInt + 1 - lo.toInt).toNat }

instance Int8.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int8

instance Int8.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int8

instance Int8.instRxoHasSize : Std.Rxo.HasSize Int8

Equations

• Int8.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance Int8.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int8

instance Int8.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int8

instance Int8.instRxiHasSize : Std.Rxi.HasSize Int8

Equations

• Int8.instRxiHasSize = { size := fun (lo : Int8) => (2 ^ 7 - lo.toInt).toNat }

instance Int8.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int8

instance Int8.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int8

instance Int16.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int16

Equations

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

instance Int16.instRxcHasSize : Std.Rxc.HasSize Int16

Equations

• Int16.instRxcHasSize = { size := fun (lo hi : Int16) => (hi.toInt + 1 - lo.toInt).toNat }

instance Int16.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int16

instance Int16.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int16

instance Int16.instRxoHasSize : Std.Rxo.HasSize Int16

Equations

• Int16.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance Int16.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int16

instance Int16.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int16

instance Int16.instRxiHasSize : Std.Rxi.HasSize Int16

Equations

• Int16.instRxiHasSize = { size := fun (lo : Int16) => (2 ^ 15 - lo.toInt).toNat }

instance Int16.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int16

instance Int16.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int16

instance Int32.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int32

Equations

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

instance Int32.instRxcHasSize : Std.Rxc.HasSize Int32

Equations

• Int32.instRxcHasSize = { size := fun (lo hi : Int32) => (hi.toInt + 1 - lo.toInt).toNat }

instance Int32.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int32

instance Int32.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int32

instance Int32.instRxoHasSize : Std.Rxo.HasSize Int32

Equations

• Int32.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance Int32.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int32

instance Int32.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int32

instance Int32.instRxiHasSize : Std.Rxi.HasSize Int32

Equations

• Int32.instRxiHasSize = { size := fun (lo : Int32) => (2 ^ 31 - lo.toInt).toNat }

instance Int32.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int32

instance Int32.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int32

instance Int64.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int64

Equations

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

instance Int64.instRxcHasSize : Std.Rxc.HasSize Int64

Equations

• Int64.instRxcHasSize = { size := fun (lo hi : Int64) => (hi.toInt + 1 - lo.toInt).toNat }

instance Int64.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int64

instance Int64.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Int64

instance Int64.instRxoHasSize : Std.Rxo.HasSize Int64

Equations

• Int64.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance Int64.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize Int64

instance Int64.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite Int64

instance Int64.instRxiHasSize : Std.Rxi.HasSize Int64

Equations

• Int64.instRxiHasSize = { size := fun (lo : Int64) => (2 ^ 63 - lo.toInt).toNat }

instance Int64.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize Int64

instance Int64.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite Int64

instance ISize.instUpwardEnumerable : Std.PRange.UpwardEnumerable ISize

Equations

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

instance ISize.instRxcHasSize : Std.Rxc.HasSize ISize

Equations

• ISize.instRxcHasSize = { size := fun (lo hi : ISize) => (hi.toInt + 1 - lo.toInt).toNat }

instance ISize.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize ISize

instance ISize.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite ISize

instance ISize.instRxoHasSize : Std.Rxo.HasSize ISize

Equations

• ISize.instRxoHasSize = Std.Rxo.HasSize.ofClosed

instance ISize.instRxoLawfulHasSize : Std.Rxo.LawfulHasSize ISize

instance ISize.instRxoIsAlwaysFinite : Std.Rxo.IsAlwaysFinite ISize

instance ISize.instRxiHasSize : Std.Rxi.HasSize ISize

Equations

• ISize.instRxiHasSize = { size := fun (lo : ISize) => (2 ^ (System.Platform.numBits - 1) - lo.toInt).toNat }

instance ISize.instRxiLawfulHasSize : Std.Rxi.LawfulHasSize ISize

instance ISize.instRxiIsAlwaysFinite : Std.Rxi.IsAlwaysFinite ISize