def same_pair.go

lawful-bytes@0.1.1.0 · PROOF.bend:171

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B
import lawful-bytes@0.1.1.0/proof_core.bend as C
import lawful-bytes@0.1.1.0/proof_same.bend as S

171def same_pair.go(-a: D.Bytes, -b: D.Bytes, +i: U32, +j: U32, +n: U32, m_a: C.BMirror(a), m_b: C.BMirror(b)) ->
172  {B.same(a, i, b, j, n) == (a, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(a, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}:
173  (+l_a, m2_a) = m_a
174  (+t_a, +e_a) = m2_a
175  (+l_b, m2_b) = m_b
176  (+t_b, +e_b) = m2_b
177  %e_a : {B.same(_, i, b, j, n) == (_, (b, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(_, i, b, j, n))))) : D.Bytes & (D.Bytes & Bool)}
178  %e_b : {B.same(C.BT(l_a, t_a), i, _, j, n) == (C.BT(l_a, t_a), (_, Pair.snd(D.Bytes, Bool, Pair.snd(D.Bytes, D.Bytes & Bool, B.same(C.BT(l_a, t_a), i, _, j, n))))) : D.Bytes & (D.Bytes & Bool)}
179  S.same_pair_t(l_a, t_a, l_b, t_b, i, j, n)