def adc_sub_add

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1371

import Base

1371def adc_sub_add(n: Nat, a: Word(n), b: Word(n), c: Bool) -> {a == Word.adc(n, Word.adc(n, a, b, True{}, c), b, False{}, Bool.not(c)) : Word(n)}:
1372  match n:
1373    case 0n:
1374      match a:
1375        case WNil{}:
1376          {==}
1377    case 1n+p:
1378      match a b c:
1379        case WCon{True{}, at} WCon{True{}, bt} True{}:
1380          %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
1381          {==}
1382        case WCon{True{}, at} WCon{True{}, bt} False{}:
1383          %adc_sub_add(p, at, bt, False{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
1384          {==}
1385        case WCon{True{}, at} WCon{False{}, bt} True{}:
1386          %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
1387          {==}
1388        case WCon{True{}, at} WCon{False{}, bt} False{}:
1389          %adc_sub_add(p, at, bt, True{}) : {WCon{True{}, at} == WCon{True{}, _} : Word(1n+p)}
1390          {==}
1391        case WCon{False{}, at} WCon{True{}, bt} True{}:
1392          %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
1393          {==}
1394        case WCon{False{}, at} WCon{True{}, bt} False{}:
1395          %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
1396          {==}
1397        case WCon{False{}, at} WCon{False{}, bt} True{}:
1398          %adc_sub_add(p, at, bt, True{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
1399          {==}
1400        case WCon{False{}, at} WCon{False{}, bt} False{}:
1401          %adc_sub_add(p, at, bt, False{}) : {WCon{False{}, at} == WCon{False{}, _} : Word(1n+p)}
1402          {==}