N = 1_{⊥}⊕NS = A⊗S_{⊥}D = N⊕[DD]_{⊥}C = R^{C}×C

(−)_{⊥} ⊕ ⊗ 1 = ≅ N ⊥ A M_{⊥} M S M M D D ⊥_{D} D D ⊥_{D} \underline{λ}d:D.⊥_{D}

C = R^{C}×C C R^{C} ≅

R^{R^{C}×C} ≅ (R^{C})^{(R^{C})}

D = D^{D} R D = F (D, D)

F locally continuous

×

strict F : (Y_{2}, Y_{1})×

(X_{1}, X_{2})(F (Y_{1}, X_{1}), F (Y_{2}, X_{2}))

X_{1} X_{2} Y_{1} Y_{2} 1 ⊥ (−)_{⊥} × ⊗ + ⊕

F :^{×} bifree solution of

X = F (X, X)

D α : F (D, D)D e : DD e = α∘ F (e, e)∘

α^{−1} D F :^{×} α : F (A, A)A

β : F (B, B)B

X = F (X, X)

If A and B are domains then their smash product A⊗ B consists of all pairs (a, b) ∈ A×B with a=⊥∨ b=⊥ ⇒ a=⊥=b and the order on A⊗B is inherited from A×B.