[STATEMENT]
lemma determI[intro]:
  "\<lbrakk> additive t; maximal t \<rbrakk> \<Longrightarrow> determ t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Transformers.additive t; maximal t\<rbrakk> \<Longrightarrow> determ t
[PROOF STEP]
by(simp add:determ_def)