:: deftheorem Def24 defines degenerated AOFA_000:def 24 :
for A being preIfWhileAlgebra holds
( A is degenerated iff ( ex I1, I2 being Element of A st
( ( I1 <> EmptyIns A & I1 \; I2 = I2 ) or ( I2 <> EmptyIns A & I1 \; I2 = I1 ) or ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) or ex C, I1, I2 being Element of A st if-then-else (C,I1,I2) = EmptyIns A or ex C, I being Element of A st while (C,I) = EmptyIns A or ex I1, I2, C, J1, J2 being Element of A st
( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = if-then-else (C,J1,J2) ) or ex I1, I2, C, J being Element of A st
( I1 <> EmptyIns A & I2 <> EmptyIns A & I1 \; I2 = while (C,J) ) or ex C1, I1, I2, C2, J being Element of A st if-then-else (C1,I1,I2) = while (C2,J) ) );