~/jendhub

law word_comparison_step

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/string_compare.bend:62

import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as StringCompare
import Base

62law word_comparison_step:
63  for n: Nat
64  for a: Word(n)
65  for b: Word(n)
66  for c: Cmp
67  for x: Bool
68  for y: Bool
69  for proof: comparison_identity(Word(n), a, b, c)
70  comparison_identity(Word(1n+n), WCon{x, a}, WCon{y, b}, Word.cmp.fin(x, y, c))

Uses (9)

Used by (1)