~/jendhub

def un.sh

bend-osdev-u32@0.1.0.0 · PROOF.bend:526

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
import Base

526# 1 + (2A + (1 + 2B)) = 2 + (2A + 2B)
527def un.sh(+a: Nat, +b: Nat) -> {2n+Nat.add(Nat.double(a), Nat.double(b)) == 1n+Nat.add(Nat.double(a), 1n+Nat.double(b)) : Nat}:
528  un.succ_cong(1n+Nat.add(Nat.double(a), Nat.double(b)), Nat.add(Nat.double(a), 1n+Nat.double(b)), Equal.sym(Nat, Nat.add(Nat.double(a), 1n+Nat.double(b)), 1n+Nat.add(Nat.double(a), Nat.double(b)), un.add_succ(Nat.double(a), Nat.double(b))))

Uses (6)

Used by (1)