equal
deleted
inserted
replaced
138 "\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t) |
138 "\<forall>s a t. (P s) \<and> s \<midarrow>a\<midarrow>A\<rightarrow> t \<longrightarrow> (Q t) |
139 \<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t) |
139 \<Longrightarrow> ex \<TTurnstile> (Init (\<lambda>(s, a, t). P s) \<^bold>\<and> Init (\<lambda>(s, a, t). s \<midarrow>a\<midarrow>A\<rightarrow> t) |
140 \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))" |
140 \<^bold>\<longrightarrow> (\<circle>(Init (\<lambda>(s, a, t). Q s))))" |
141 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) |
141 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def) |
142 apply clarify |
142 apply clarify |
143 apply (simp split add: if_split) |
143 apply (simp split: if_split) |
144 text \<open>\<open>TL = UU\<close>\<close> |
144 text \<open>\<open>TL = UU\<close>\<close> |
145 apply (rule conjI) |
145 apply (rule conjI) |
146 apply (pair ex) |
146 apply (pair ex) |
147 apply (Seq_case_simp x2) |
147 apply (Seq_case_simp x2) |
148 apply (pair a) |
148 apply (pair a) |