~/jendhub

law reify_node

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/blake/blake2s/array.bend:18

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/array.bend as Array
import Base

18law reify_node:
19  for -l: Array<U32>
20  for -r: Array<U32>
21  for left: Sigma<&2,&1,Tree,t => {l == thaw(t) : Array<U32>}>
22  for right: Sigma<&2,&1,Tree,t => {r == thaw(t) : Array<U32>}>
23  Sigma<&2,&1,Tree,t => {ANode{l,r} == thaw(t) : Array<U32>}>

Uses (7)

Used by (1)