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.

@[implicit_reducible]

instance Int8.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int8

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Int16.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int16

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Int32.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int32

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Int64.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int64

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance ISize.instUpwardEnumerable : Std.PRange.UpwardEnumerable ISize

Equations

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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