theory Beta imports Main begin typedecl L consts betas :: "L \ L \ bool" definition normal :: L \ bool where "normal t = \ u, betas t u \ t=u" definition confluent :: bool where "confluent = (\ t u v. (betas t u \ betas t v) \ (\ w . (betas t w \ betas v w)))" definition has_normal :: L \ bool where "has_normal t = \ u, betas t u \ normal u" prop "(\ t. \ u. betas t u \ \ (normal u))" end