The Theory xl-mm1

Parents

gst

Constants

	GS
InferProp	GS
ProgProp	GS
DocProp	GS
Specification	GS
Program	GS
Language	GS
Document	GS
mk_ip	GS GS GS GS
mk_pp	GS GS GS
mk_dp	GS GS GS
mk_spec	GS GS GS
ip_out	GS GS
ip_in	GS GS
ip_prog	GS GS
pp_prog	GS GS
pp_spec	GS GS
dp_doc	GS GS
dp_lang	GS GS
out_lang	GS GS
in_lang	GS GS
TrueDocP	GS BOOL
DocInferP	GS BOOL
SoundProgP	GS BOOL

Definitions

Document Language Program Specification DocProp ProgProp InferProp	_g Document Language = _g Document Program = Document _g Document Specification = Language _g Language DocProp = Language _g Document ProgProp = Specification _g Program InferProp = Program _g Document _g Document
mk_spec mk_dp mk_pp mk_ip	mk_spec = $_g mk_dp = $_g mk_pp = $_g mk_ip = ( pr inp out pr _g inp _g out)
in_lang out_lang dp_lang dp_doc pp_spec pp_prog ip_prog ip_in ip_out	in_lang = fst out_lang = snd dp_lang = fst dp_doc = snd pp_spec = fst pp_prog = snd ip_prog = fst ip_in = ( d fst (snd d)) ip_out = ( d snd (snd d))
TrueDocP	dp TrueDocP dp dp _g DocProp dp_doc dp _g dp_lang dp
DocInferP	ip DocInferP ip ip _g InferProp ip_in ip _g ip_out ip _g ip_prog ip
SoundProgP	pp SoundProgP pp pp _g ProgProp ( ind oud TrueDocP (mk_dp (in_lang (pp_spec pp)) ind) DocInferP (mk_ip (pp_prog pp) ind oud) TrueDocP (mk_dp (out_lang (pp_spec pp)) oud))

Theorems

id_spec_thm	l l _g Language SoundProgP ((l _g l) _g id l)
mm1_mp_thm	in_doc in_lan p out_doc out_lan TrueDocP (mk_dp in_lan in_doc) SoundProgP (mk_pp (mk_spec in_lan out_lan) p) DocInferP (mk_ip p in_doc out_doc) TrueDocP (mk_dp out_lan out_doc)
mm1_mpc_thm	d1 l1 d2 l2 d3 l3 p1 p2 TrueDocP (mk_dp l1 d1) SoundProgP (mk_pp (mk_spec l1 l2) p1) SoundProgP (mk_pp (mk_spec l2 l3) p2) DocInferP (mk_ip p1 d1 d2) DocInferP (mk_ip p2 d2 d3) TrueDocP (mk_dp l3 d3)

V