Up to index of Isabelle/HOL/raw-confluence-lambda
theory AlphaBetaDiamond = Commutation + WeakABComm + FreshAlphaConf + DiamondPB + ExistsBCF(* Title: AlphaBetaDiamond.thy Author: James Brotherston / Rene Vestergaard Revised: 30th August, 2000 - Choice of the "middle relation" in Nipkow's confluence result as ->>A; -|>B *) AlphaBetaDiamond = Commutation + WeakABComm + FreshAlphaConf + DiamondPB + ExistsBCF + consts relation2 :: "(lterm * lterm) set" syntax "->2" :: [lterm,lterm] => bool (infixl 50) translations "s ->2 t" == "(s,t) : relation2" inductive relation2 intrs cons "[|e1 ->>A e2; e2 -|>B e3|] ==> e1 ->2 e3" end
theorem diamond_relation2:
diamond relation2