def AP.z2

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

import Base

462def AP.z2(n: Nat, d: Nat) -> {Word.adc(n, AP.pw(n, d), Word.zero(n), True{}, False{}) == AP.lm(n, d) : Word(n)}:
463  match n:
464    case 0n:
465      {==}
466    case 1n+ +q:
467      match d:
468        case 0n:
469          AP.wcon_cong(q, False{}, Word.adc(q, Word.zero(q), Word.zero(q), True{}, True{}), Word.zero(q), AP.z1(q))
470        case 1n+ +e:
471          AP.wcon_cong(q, True{}, Word.adc(q, AP.pw(q, e), Word.zero(q), True{}, False{}), AP.lm(q, e), AP.z2(q, e))