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.

翻译：我们使用一种基于计算路径（重写序列）概念的标记演绎系统（LND$_{ED-}$TRS），将计算路径作为同一类型两个项之间的相等关系，这使得我们能够在同伦论中运用计算路径概念展开一种方法。由此，我们证明计算路径可用于执行$LND_{EQ}-TRS_{2}$重写系统的证明。