Session Lisa
More information about this formalization is available
here
.
View
theory dependencies
Theories
LS_Extras
(term rewriting notions and utilities)
LS_Prelude
(layer conditions)
LS_Basics
(basic results on layer systems)
LS_Common
(preparation for main results)
LS_General
(main result for general TRSs)
LS_Modularity
(modularity application)
LS_Persistence
(persistence application)
LS_Currying
(currying application, part 1)
LS_Currying2
(currying application, part 2)
LS_Left_Linear
(main result for left-linear TRSs)
LS_Bounded_Duplicating
(unfinished)
LS_Persistence_Impl
(executable version of persistent decomposition)