def gt.add_zero

bend-osdev-gf@0.1.1.0 · proof_tab.bend:98

import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab

import Base

98def gt.add_zero(x: U32) -> {U32.add(x, 0) == x : U32}:
99  match x:
100    case U32{+w}:
101      gt.u32_cong(Word.adc(32n, w, Word.zero(32n), False{}, False{}), w, gt.adc_zero(32n, w))

Uses (7)

Used by (2)