let A be preIfWhileAlgebra; :: thesis: ( A is free implies ( A is well_founded & not A is degenerated ) )
assume A1: A is free ; :: thesis: ( A is well_founded & not A is degenerated )
then reconsider A9 = A as free Universal_Algebra ;
set G = the free GeneratorSet of A9;
Generators A = the free GeneratorSet of A9 by Th34;
hence ElementaryInstructions A is GeneratorSet of A by Th31, Th71; :: according to AOFA_000:def 25 :: thesis: not A is degenerated
thus for I1, I2 being Element of A holds
( not ( I1 <> EmptyIns A & I1 \; I2 = I2 ) & not ( I2 <> EmptyIns A & I1 \; I2 = I1 ) & not ( ( I1 <> EmptyIns A or I2 <> EmptyIns A ) & I1 \; I2 = EmptyIns A ) ) by A1, Th72, Th73; :: according to AOFA_000:def 24 :: thesis: ( ( for C, I1, I2 being Element of A holds not if-then-else (C,I1,I2) = EmptyIns A ) & ( for C, I being Element of A holds not while (C,I) = EmptyIns A ) & ( for I1, I2, C, J1, J2 being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = if-then-else (C,J1,J2) ) ) & ( for I1, I2, C, J being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = while (C,J) ) ) & ( for C1, I1, I2, C2, J being Element of A holds not if-then-else (C1,I1,I2) = while (C2,J) ) )
thus ( ( for C, I1, I2 being Element of A holds not if-then-else (C,I1,I2) = EmptyIns A ) & ( for C, I being Element of A holds not while (C,I) = EmptyIns A ) & ( for I1, I2, C, J1, J2 being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = if-then-else (C,J1,J2) ) ) & ( for I1, I2, C, J being Element of A holds
( not I1 <> EmptyIns A or not I2 <> EmptyIns A or not I1 \; I2 = while (C,J) ) ) & ( for C1, I1, I2, C2, J being Element of A holds not if-then-else (C1,I1,I2) = while (C2,J) ) ) by A1, Th72, Th73, Th74; :: thesis: verum