let A be ECIW-strict preIfWhileAlgebra; for x being set
for n being Nat holds
( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
set B = ElementaryInstructions A;
let x be set ; for n being Nat holds
( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
let n be Nat; ( not x in (ElementaryInstructions A) |^ (n + 1) or x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
assume A1:
x in (ElementaryInstructions A) |^ (n + 1)
; ( x in (ElementaryInstructions A) |^ n or x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
then reconsider I = x as Element of A ;
assume A2:
x nin (ElementaryInstructions A) |^ n
; ( x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
assume A3:
x <> EmptyIns A
; ( ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
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 )
; ( ex C, I1, I2 being Element of A st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions A) |^ n & I1 in (ElementaryInstructions A) |^ n & I2 in (ElementaryInstructions A) |^ n ) or ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n ) )
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 )
; ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n )
(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
( o = 1 or o = 2 or o = 3 or o = 4 )
by Th55;
suppose A17:
o = 2
;
ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n )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;
verum end; suppose A22:
o = 3
;
ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n )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;
verum end; suppose A28:
o = 4
;
ex C, I being Element of A st
( x = while (C,I) & C in (ElementaryInstructions A) |^ n & I in (ElementaryInstructions A) |^ n )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;
verum end; end;