def subtract_compared

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:90

import Base
import stelliferous@0.0.2.0/proofs/word_subtraction.bend as Subtraction

90def subtract_compared(+left: U32,+right: U32,+offset: U32,equal: Bool,
91  compared: {U32.is_eq((left - offset : U32),(right - offset : U32)) == equal : Bool},different: {U32.is_eq(left,right) == False{} : Bool}) -> {equal == False{} : Bool}:
92  match equal:
93    case False{}: {==}
94    case True{}:
95      Empty.absurd({True{} == False{} : Bool},unequal_words(left,right,different,
96        Equal.trans(U32,left,((left - offset : U32) + offset : U32),right,
97          Equal.sym(U32,((left - offset : U32) + offset : U32),left,Subtraction.add_subtract(left,offset)),
98          Equal.trans(U32,((left - offset : U32) + offset : U32),((right - offset : U32) + offset : U32),right,
99            Equal.cong(U32,U32,value => (value + offset : U32),(left - offset : U32),(right - offset : U32),equal_words((left - offset : U32),(right - offset : U32),compared)),
100            Subtraction.add_subtract(right,offset)))))