def unequal_words
stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:84
import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
84def unequal_words(+left: U32,+right: U32,different: {U32.is_eq(left,right) == False{} : Bool},equal: {left == right : U32}) -> Empty:
85 WordEncoding.false_true(Equal.trans(Bool,False{},U32.is_eq(left,right),True{},Equal.sym(Bool,U32.is_eq(left,right),False{},different),
86 %equal : {U32.is_eq(left,_) == True{} : Bool}
87 %Equal.sym(Bool,U32.is_eq(left,left),Nat.is_eq(U32.to_nat(left),U32.to_nat(left)),Comparison.eq(left,left)) : {_ == True{} : Bool}
88 Order.equal_reflexive(U32.to_nat(left))))