lemma asig_triple_proj: "outputs (a, b, c) = b \ inputs (a, b, c) = a \<and> internals (a, b, c) = c" by (simp add: asig_projections)
lemma int_and_ext_is_act: "a \ internals S \ a \ externals S \ a \ actions S" by (simp add: externals_def actions_def)
lemma ext_is_act: "a \ externals S \ a \ actions S" by (simp add: externals_def actions_def)
lemma int_is_act: "a \ internals S \ a \ actions S" by (simp add: asig_internals_def actions_def)
lemma inp_is_act: "a \ inputs S \ a \ actions S" by (simp add: asig_inputs_def actions_def)
lemma out_is_act: "a \ outputs S \ a \ actions S" by (simp add: asig_outputs_def actions_def)
lemma ext_and_act: "x \ actions S \ x \ externals S \ x \ externals S" by (fast intro!: ext_is_act)
lemma not_ext_is_int: "is_asig S \ x \ actions S \ x \ externals S \ x \ internals S" by (auto simp add: actions_def is_asig_def externals_def)
lemma not_ext_is_int_or_not_act: "is_asig S \ x \ externals S \ x \ internals S \x \ actions S" by (auto simp add: actions_def is_asig_def externals_def)
lemma int_is_not_ext:"is_asig S \ x \ internals S \ x \ externals S" by (auto simp add: externals_def actions_def is_asig_def)
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
