[STATEMENT]
lemma fdia_arden_iff: "\<nabla>x = 0 \<Longrightarrow> (d p = d q + |x\<rangle> p \<longleftrightarrow> d p = |x\<^sup>\<star>\<rangle> q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nabla>x = (zero_class.zero::'a) \<Longrightarrow> (d p = d q +  |x\<rangle> p) = (d p =  |x\<^sup>\<star>\<rangle> q)
[PROOF STEP]
by (metis fdia_arden_eq dka.fdia_d_simp dka.fdia_star_unfold_var)