in neural circuit with
downstream in neural circuit with
(forall (?x ?y)
(iff
(downstream_neural_circuit_path ?x ?y)
(and
("neuron ; CL_0000540" ?x)
("neuron ; CL_0000540" ?y)
(synapsed_by ?x ?y))))
(forall (...s ?x ?y ?z)
(iff
(downstream_neural_circuit_path ...s ?x ?y ?z )
(and
(downstream_neural_circuit_path ...s ?x ?y)
("neuron ; CL_0000540" ?z)
(synapsed_by ?y ?z))))
(forall (?x ?y)
(iff
(downstream_in_neural_circuit_with ?x ?y)
(exists (...s)
(downstream_neural_circuit_path ?x ...s ?y))))
A relation that holds between a neuron that is synapsed_to another neuron or a neuron that is connected indirectly to another by a chain of neurons, each synapsed_to the next.
David Osumi-Sutherland
pending final vetting
axiom holds for all times