Using Formal Verification to Prove Properties of Lists Recursively Defined

We define finite integer lists recursively and verify a property calculus for their structural and arithmetic operations in Scala Stainless. The verified results establish identities for indexed access and slicing, sum and product laws under concatenation, divisibility of list products by their elements, and preservation of element bounds through append and split. We also verify shifted-list laws preserving the period and relating adjacent values to gaps, together with rotation laws preserving membership, size, sum, and element bounds. Collectively, these properties describe recursive finite sequences under decomposition, composition, aggregation, bounds, periodic shifts, and rotation.