let A be ECIW-strict preIfWhileAlgebra; :: thesis:
set B = ElementaryInstructions A;
let x be set ; :: thesis:
let n be Nat; :: thesis:
assume A1: x in (ElementaryInstructions A) |^ (n + 1) ; :: thesis:
then reconsider I = x as Element of A ;
assume A2: x nin (ElementaryInstructions A) |^ n ; :: thesis:
assume A3: x <> EmptyIns A ; :: thesis:
assume A4: for I1, I2 being Element of A holds
( not x = I1 \; I2 or not I1 in (ElementaryInstructions A) |^ n or not I2 in (ElementaryInstructions A) |^ n ) ; :: thesis:
assume A5: for C, I1, I2 being Element of A holds
( not x = if-then-else (C,I1,I2) or not C in (ElementaryInstructions A) |^ n or not I1 in (ElementaryInstructions A) |^ n or not I2 in (ElementaryInstructions A) |^ n ) ; :: thesis:
(ElementaryInstructions A) |^ (n + 1) = ((ElementaryInstructions A) |^ n) \/ { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= (ElementaryInstructions A) |^ n ) } by Th19;
then x in { ((Den (o,A)) . p) where o is Element of dom the charact of A, p is Element of the carrier of A * : ( p in dom (Den (o,A)) & rng p c= (ElementaryInstructions A) |^ n ) } by A1, A2, XBOOLE_0:def 3;
then consider o being Element of dom the charact of A, p being Element of the carrier of A * such that
A6: I = (Den (o,A)) . p and
A7: p in dom (Den (o,A)) and
A8: rng p c= (ElementaryInstructions A) |^ n ;
reconsider no = o as Element of NAT ;
reconsider oo = Den (o,A) as Element of Operations A ;
len (signature A) = len the charact of A by UNIALG_1:def 4;
then A9: dom (signature A) = dom the charact of A by FINSEQ_3:29;
A10: len p = arity oo by A7, MARGREL1:def 25
.= (signature A) . no by A9, UNIALG_1:def 4
.= ECIW-signature . o by Def27 ;
A11: 1 in Seg 2 ;
A12: 2 in Seg 2 ;
A13: 1 in Seg 3 ;
A14: 2 in Seg 3 ;
A15: 3 in Seg 3 ;

per cases by Th55;

suppose A16: o = 1 ; :: thesis:

then p = {} by A10, Th54;
hence ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A3, A6, A16; :: thesis:

end;

suppose A17: o = 2 ; :: thesis:

then A18: p = <*(p . 1),(p . 2)*> by A10, Th54, FINSEQ_1:44;
A19: dom p = Seg 2 by A10, A17, Th54, FINSEQ_1:def 3;
then A20: p . 1 in rng p by A11, FUNCT_1:def 3;
A21: p . 2 in rng p by A12, A19, FUNCT_1:def 3;
then reconsider I1 = p . 1, I2 = p . 2 as Element of A by A20;
I = I1 \; I2 by A6, A17, A18;
hence ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A4, A8, A20, A21; :: thesis:

end;

suppose A22: o = 3 ; :: thesis:

then A23: p = <*(p . 1),(p . 2),(p . 3)*> by A10, Th54, FINSEQ_1:45;
A24: dom p = Seg 3 by A10, A22, Th54, FINSEQ_1:def 3;
then A25: p . 1 in rng p by A13, FUNCT_1:def 3;
A26: p . 2 in rng p by A14, A24, FUNCT_1:def 3;
A27: p . 3 in rng p by A15, A24, FUNCT_1:def 3;
then reconsider C = p . 1, I1 = p . 2, I2 = p . 3 as Element of A by A25, A26;
I = if-then-else (C,I1,I2) by A6, A22, A23;
hence ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A5, A8, A25, A26, A27; :: thesis:

end;

suppose A28: o = 4 ; :: thesis:

then A29: p = <*(p . 1),(p . 2)*> by A10, Th54, FINSEQ_1:44;
A30: dom p = Seg 2 by A10, A28, Th54, FINSEQ_1:def 3;
then A31: p . 1 in rng p by A11, FUNCT_1:def 3;
A32: p . 2 in rng p by A12, A30, FUNCT_1:def 3;
then reconsider I1 = p . 1, I2 = p . 2 as Element of A by A31;
I = while (I1,I2) by A6, A28, A29;
hence ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) by A8, A31, A32; :: thesis:

end;

end;