Circuit dependency graphs -- proof internals

theorem Complexity.Circuit.dependencyGraph_adj_val_lt_internal {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) {source target : Fin (N + G + M)} (edge : c.dependencyGraph.Adj source target) : ↑source < ↑target

theorem Complexity.Circuit.dependencyGraph_isAcyclic_internal {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.IsAcyclic

theorem Complexity.Circuit.dependencyGraph_edgeFinset_internal {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.edgeFinset = c.dependencyEdges

theorem Complexity.Circuit.dependencyGraph_edge_card_le_totalFanIn_internal {B : Basis} {N M G : ℕ} [NeZero N] [NeZero M] (c : Circuit B N M G) : c.dependencyGraph.edgeFinset.card ≤ c.totalFanIn