def word.cmp_nat

bend-osdev-algo@0.1.0.0 · PROOF.bend:910

import Base

910def word.cmp_nat(n: Nat, a: Word(n), b: Word(n)) -> {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}:
911  match n:
912    case 0n:
913      match a b:
914        case WNil{} WNil{}:
915          {==}
916    case 1n+ +p:
917      match a b:
918        case WCon{True{}, +at} WCon{True{}, +bt}:
919          word.cmp_nat.h(p, True{}, True{}, at, bt, word.cmp_nat(p, at, bt))
920        case WCon{True{}, +at} WCon{False{}, +bt}:
921          word.cmp_nat.h(p, True{}, False{}, at, bt, word.cmp_nat(p, at, bt))
922        case WCon{False{}, +at} WCon{True{}, +bt}:
923          word.cmp_nat.h(p, False{}, True{}, at, bt, word.cmp_nat(p, at, bt))
924        case WCon{False{}, +at} WCon{False{}, +bt}:
925          word.cmp_nat.h(p, False{}, False{}, at, bt, word.cmp_nat(p, at, bt))