(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
definition dbfr (r): relation2 prototerm prototerm ≝
λt1,t2.
∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &
(* DELAYED BALANCED FOCUSED REDUCTION ***************************************)
definition dbfr (r): relation2 prototerm prototerm ≝
λt1,t2.
∃∃p,b,q,m,n. p●𝗔◗b●𝗟◗q = r &