If $F$ has an edge, after unfolding $ForestwidthLE Δ (k - 1) F$ (the arithmetic $(k - 1) + 1 = k$, using $k ≥ 2$, is immediate) into a $DepthDecomposition F Δ k$, we split on whether $F$ has isolated vertices ($isoJ F = 0$ or not) and invoke $exists_circuit_of_noIsolated$ or $exists_circuit_of_isolated$ respectively ($exists_circuit_of_edge$). If $F$ has no edges, $hom K F n$ is the constant $n ^ |F.A| * n ^ |F.B|$ ($hom_eq_const_of_no_edge$), computed by the single-gate $constCircuit$, of size $1$.