WordMultiplication.truncate_inc: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_multiplication.bend as WordMultiplication
Lines 22-32 of stelliferous@0.0.2.0/proofs/word_multiplication.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&start_line=22&end_line=32

import Base

def truncate_inc(+n: Nat,+w: Word(1n+n)) -> {truncate(n,Word.inc(1n+n,w)) == Word.inc(n,truncate(n,w)) : Word(n)}:
  match n:
    case 0n:
      {==}
    case 1n+ +p:
      match w:
        case WCon{False{},t}:
          {==}
        case WCon{True{},+t}:
          %truncate_inc(p,t) : {WCon{False{},truncate(p,Word.inc(1n+p,t))} == WCon{False{},_} : Word(1n+p)}
          {==}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=truncate