计算路径——$LND_{EQ}-TRS_{2}$系统中的一种方法
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system
AI总结：
本文提出基于计算路径概念的标号演绎系统LND$_{ED-}$TRS，将其作为同类型项间的相等关系应用于同伦理论，并证明计算路径可用于完成$LND_{EQ}-TRS_{2}$重写系统的证明。
摘要：
我们使用基于计算路径（重写序列）概念的标号演绎系统（LND$_{ED-}$TRS），将其作为同类型两个项之间的相等关系，这使得我们能够在同伦理论中运用计算路径概念进行探索。由此，我们证明计算路径可用于完成$LND_{EQ}-TRS_{2}$重写系统的证明。
英文摘要：
We use a labelled deduction system ( LND$_{ED-}$TRS ) based on the concept of computational paths (sequences of rewrites) as equalities between two terms of the same type, which allowed us to carry out in homotopic theory an approach using the concept of computational paths. From this, we show that the computational paths can be used to perform the proofs of the $LND_{EQ}-TRS_{2}$ rewriting system.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
