~/bend-docscommunity

proofs/natural_addition.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/natural_addition.bend as Natural_addition

Shared natural-number addition laws; induction is on a symbolic operand.

1 import
import Base

Laws

law successor_right proved

Also proved in bend-mathlib as nat.add_succ: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_succ.

source · line 4 · raw

@+a:Nat -> @+b:Nat -> {Nat.add(a, 1n+b) == 1n+Nat.add(a, b) : Nat}

law double provedsource · line 17 · raw

@+n:Nat -> {Nat.add(n, n) == Nat.double(n) : Nat}

law zero_right proved

Also proved in bend-mathlib as nat.add_zero: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_zero.

source · line 30 · raw

@+n:Nat -> {Nat.add(n, 0n) == n : Nat}

law successor_width provedsource · line 42 · raw

@+width:Nat -> {Nat.add(width, 1n) == 1n+width : Nat}

law associative proved

Also proved in bend-mathlib as nat.add_assoc: import bend-mathlib@0.7.2.0/nat.bend as MNat, then MNat.add_assoc.

source · line 53 · raw

@+first:Nat -> @+second:Nat -> @+third:Nat -> {Nat.add(Nat.add(first, second), third) == Nat.add(first, Nat.add(second, third)) : Nat}