def AP.z1

bend-osdev-array@0.1.0.1 · PROOF.bend:455

import bend-osdev-array@0.1.0.1/PROOF.bend as PROOF

import Base

455def AP.z1(n: Nat) -> {Word.adc(n, Word.zero(n), Word.zero(n), True{}, True{}) == Word.zero(n) : Word(n)}:
456  match n:
457    case 0n:
458      {==}
459    case 1n+ +q:
460      AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))

Uses (6)

Used by (2)