Proof of `L ⊆ NL`
groundedproofs/Lax485149Proofs/Bridge.lean · lax-485149
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
An FO(DTC) definable problem is FO(TC) definable, and FO(TC) definability is membership in NL, both by this submission's statements.