def AP.nc

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

import Base

123def AP.nc(x: Nat, y: Nat, a: Bool, b: Bool) -> {Nat.cmp(AP.bv(a, x), AP.bv(b, y)) == Word.cmp.fin(a, b, Nat.cmp(x, y)) : Cmp}:
124  match x y:
125    case 0n 0n:
126      match a b:
127        case False{} False{}:
128          {==}
129        case False{} True{}:
130          {==}
131        case True{} False{}:
132          {==}
133        case True{} True{}:
134          {==}
135    case 0n 1n+q:
136      match a b:
137        case False{} False{}:
138          {==}
139        case False{} True{}:
140          {==}
141        case True{} False{}:
142          {==}
143        case True{} True{}:
144          {==}
145    case 1n+p 0n:
146      match a b:
147        case False{} False{}:
148          {==}
149        case False{} True{}:
150          {==}
151        case True{} False{}:
152          {==}
153        case True{} True{}:
154          {==}
155    case 1n+p 1n+q:
156      match a b:
157        case False{} False{}:
158          AP.nc(p, q, False{}, False{})
159        case False{} True{}:
160          AP.nc(p, q, False{}, True{})
161        case True{} False{}:
162          AP.nc(p, q, True{}, False{})
163        case True{} True{}:
164          AP.nc(p, q, True{}, True{})