theory Scheduler_IF

lemma equiv_valid_2_unobservable:
  assumes fI: "\<And>st. \<lbrace>P and I st and A st\<rbrace> f \<lbrace>\<lambda>_. I st\<rbrace>"
  assumes fA: "\<And>st. \<lbrace>P' and I st and A st\<rbrace> f \<lbrace>\<lambda>_. A st\<rbrace>"
  assumes gI: "\<And>st. \<lbrace>S and I st and A st\<rbrace> g \<lbrace>\<lambda>_. I st\<rbrace>"
  assumes gA: "\<And>st. \<lbrace>S' and I st and A st\<rbrace> g \<lbrace>\<lambda>_. A st\<rbrace>"
  assumes sym: "\<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s"
  assumes trans: "\<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''"
  shows "equiv_valid_2 I A A dc (P and P') (S and S') (f:: 'a \<Rightarrow> (unit \<times> 'a) set \<times> bool) g" apply (clarsimp simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def) apply (erule preserves_equivalence_2_weak,assumption) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule fI) apply (rule fA) apply force apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (rule gI) apply (rule gA) apply force apply (fastforce intro!: sym trans)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A dc (P and P') (S and S') f g proof (prove)
goal (1 subgoal):
 1. \<And>s t b a ba. \<lbrakk>((), b) \<in> fst (f s); (a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I b ba \<and> A b ba proof (prove)
goal (7 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> f \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 2. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?P23 s t b a ba s
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (8 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?Q32 s t b a ba st\<rbrace> f \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 2. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?P23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> ?Q32 s t b a ba st sa
 3. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?P23 s t b a ba s
 8. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (9 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P35 s t b a ba st\<rbrace> f \<lbrace>\<lambda>rv. I st\<rbrace>
 2. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 s t b a ba st\<rbrace> f \<lbrace>\<lambda>rv. A st\<rbrace>
 3. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?P23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> ?P35 s t b a ba st sa \<and> ?P'35 s t b a ba st sa
 4. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 8. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?P23 s t b a ba s
 9. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (8 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P'35 s t b a ba st\<rbrace> f \<lbrace>\<lambda>rv. A st\<rbrace>
 2. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?P23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> (P and I st and A st) sa \<and> ?P'35 s t b a ba st sa
 3. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?P23 s t b a ba s
 8. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (7 subgoals):
 1. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?P23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> (P and I st and A st) sa \<and> (P' and I st and A st) sa
 2. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?P23 s t b a ba s
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (6 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 2. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (7 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?Q44 s t b a ba st\<rbrace> g \<lbrace>\<lambda>_ a. I st a \<and> A st a\<rbrace>
 2. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> ?Q44 s t b a ba st sa
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (8 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P47 s t b a ba st\<rbrace> g \<lbrace>\<lambda>rv. I st\<rbrace>
 2. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P'47 s t b a ba st\<rbrace> g \<lbrace>\<lambda>rv. A st\<rbrace>
 3. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> ?P47 s t b a ba st sa \<and> ?P'47 s t b a ba st sa
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 8. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (7 subgoals):
 1. \<And>s t b a ba st. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<lbrace>?P'47 s t b a ba st\<rbrace> g \<lbrace>\<lambda>rv. A st\<rbrace>
 2. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> (S and I st and A st) sa \<and> ?P'47 s t b a ba st sa
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 7. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (6 subgoals):
 1. \<And>s t b a ba st sa. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t; (?S23 s t b a ba and (\<lambda>a. I st a \<and> A st a)) sa\<rbrakk> \<Longrightarrow> (S and I st and A st) sa \<and> (S' and I st and A st) sa
 2. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 6. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> ?S23 s t b a ba t proof (prove)
goal (5 subgoals):
 1. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s'. I s s' \<and> A s s' \<longrightarrow> I s' s \<and> A s' s
 2. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> \<forall>s s' s''. I s s' \<and> A s s' \<longrightarrow> I s' s'' \<and> A s' s'' \<longrightarrow> I s s'' \<and> A s s''
 3. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> I s t \<and> A s t
 4. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> P s \<and> P' s
 5. \<And>s t b a ba. \<lbrakk>(a, ba) \<in> fst (g t); P s; P' s; S t; S' t; I s t; A s t\<rbrakk> \<Longrightarrow> S t \<and> S' t proof (prove)
goal:
No subgoals!