World subsumption

From The Twelf Project

Jump to: navigation, search

World subsumption is a sufficient condition that a metatheorem proved for one set of LF contexts can be reused in another set of contexts.

Eventually, this page will contain a self-contained explanation for world subsumption. For now, please read the discussion in Proving totality assertions in non-empty contexts in the tutorial Proving metatheorems with Twelf and on the %worlds page.

This page is incomplete. We should expand it.
Retrieved from "http://twelf.plparty.org/wiki/World_subsumption"
Personal tools