MonotoneMapβ βAβ βBβ βRβ βSβ βf\textbf{MonotoneMap} \; A \; B \; R \; S \; fMonotoneMapABRSf
β(x,yβA::f(β{x,y})β ββ ΜΈβ ββ{f.x,f.y})\exists( x,y \in A :: f(\sqcup \{x,y\}) \; \not \cong \; \sqcup \{f.x, f.y \})β(x,yβA::f(β{x,y})ξ β β{f.x,f.y})
pred HasGenerativeEffect(A,B: set univ, R,S,f: univ->univ) { MonotoneMap[A,B,R,S,f] some x,y: A { not Equivalent[ B,S, f[Join[A,R,x+y]], Join[B,S,f[x]+f[y]] ] } }
Last updated 8 months ago