~/jendhub

def add_associative

stelliferous@0.0.2.0 · proofs/bounded_u32_arithmetic.bend:63

import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic
import Base

63def add_associative(+a: U32,+b: U32,+c: U32) -> {((a + b : U32) + c : U32) == (a + (b + c : U32) : U32) : U32}:
64  %native_roundtrip(a) : {((_ + b : U32) + c : U32) == (_ + (b + c : U32) : U32) : U32}
65  %native_roundtrip(b) : {((U32.from_nat(U32.to_nat(a)) + _ : U32) + c : U32) == (U32.from_nat(U32.to_nat(a)) + (_ + c : U32) : U32) : U32}
66  %native_roundtrip(c) : {((U32.from_nat(U32.to_nat(a)) + U32.from_nat(U32.to_nat(b)) : U32) + _ : U32) == (U32.from_nat(U32.to_nat(a)) + (U32.from_nat(U32.to_nat(b)) + _ : U32) : U32) : U32}
67  encoded_add_associative(U32.to_nat(a),U32.to_nat(b),U32.to_nat(c))

Uses (6)

Used by (3)