set B = ElementaryInstructions F1();
A2:
(ElementaryInstructions F1()) |^ 0 = ElementaryInstructions F1()
by Th18;
set FB = { [I,F4(I)] where I is Element of F1() : I in ElementaryInstructions F1() } ;
deffunc H1( Nat, set ) -> set = { [(I1 \; I2),F5(fI1,fI2)] where I1, I2 is Element of F1(), fI1, fI2 is Element of F2() : ( I1 in (ElementaryInstructions F1()) |^ $1 & I2 in (ElementaryInstructions F1()) |^ $1 & [I1,fI1] in $2 & [I2,fI2] in $2 ) } ;
deffunc H2( Nat, set ) -> set = { [(if-then-else (C,I1,I2)),F7(fC,fI1,fI2)] where C, I1, I2 is Element of F1(), fC, fI1, fI2 is Element of F2() : ( C in (ElementaryInstructions F1()) |^ $1 & I1 in (ElementaryInstructions F1()) |^ $1 & I2 in (ElementaryInstructions F1()) |^ $1 & [C,fC] in $2 & [I1,fI1] in $2 & [I2,fI2] in $2 ) } ;
deffunc H3( Nat, set ) -> set = { [(while (C,I)),F6(gC,gI)] where C, I is Element of F1(), gC, gI is Element of F2() : ( C in (ElementaryInstructions F1()) |^ $1 & I in (ElementaryInstructions F1()) |^ $1 & [C,gC] in $2 & [I,gI] in $2 ) } ;
deffunc H4( Nat, set ) -> set = ((($2 \/ {[(EmptyIns F1()),F3()]}) \/ H1($1,$2)) \/ H2($1,$2)) \/ H3($1,$2);
consider FF being Function such that
A3:
( dom FF = NAT & FF . 0 = { [I,F4(I)] where I is Element of F1() : I in ElementaryInstructions F1() } )
and
A4:
for n being Nat holds FF . (n + 1) = H4(n,FF . n)
from NAT_1:sch 11();
set f = Union FF;
A5:
for n, m being Nat st n <= m holds
FF . n c= FF . m
proof
let n,
m be
Nat;
( n <= m implies FF . n c= FF . m )
assume
n <= m
;
FF . n c= FF . m
then consider i being
Nat such that A6:
m = n + i
by NAT_1:10;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
A7:
m = n + i
by A6;
defpred S1[
Nat]
means FF . n c= FF . (n + $1);
A8:
S1[
0 ]
;
A9:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )reconsider n9 =
n as
Element of
NAT by ORDINAL1:def 12;
FF . ((n9 + i) + 1) =
H4(
n9 + i,
FF . (n9 + i))
by A4
.=
(((FF . (n + i)) \/ {[(EmptyIns F1()),F3()]}) \/ H1(n + i,FF . (n + i))) \/ (H2(n + i,FF . (n + i)) \/ H3(n + i,FF . (n + i)))
by XBOOLE_1:4
.=
((FF . (n + i)) \/ {[(EmptyIns F1()),F3()]}) \/ (H1(n + i,FF . (n + i)) \/ (H2(n + i,FF . (n + i)) \/ H3(n + i,FF . (n + i))))
by XBOOLE_1:4
.=
(FF . (n + i)) \/ ({[(EmptyIns F1()),F3()]} \/ (H1(n + i,FF . (n + i)) \/ (H2(n + i,FF . (n + i)) \/ H3(n + i,FF . (n + i)))))
by XBOOLE_1:4
;
then
FF . (n + i) c= FF . ((n + i) + 1)
by XBOOLE_1:7;
hence
(
S1[
i] implies
S1[
i + 1] )
by XBOOLE_1:1;
verum end;
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(A8, A9);
hence
FF . n c= FF . m
by A7;
verum
end;
defpred S1[ Nat] means ex g being Function of ((ElementaryInstructions F1()) |^ $1),F2() st
( g = FF . $1 & ( EmptyIns F1() in (ElementaryInstructions F1()) |^ $1 implies g . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ $1 holds
g . (I1 \; I2) = F5((g . I1),(g . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ $1 holds
g . (if-then-else (C,I1,I2)) = F7((g . C),(g . I1),(g . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ $1 holds
g . (while (C,I)) = F6((g . C),(g . I)) ) );
defpred S2[ set ] means $1 in ElementaryInstructions F1();
reconsider f0 = { [I,F4(I)] where I is Element of F1() : S2[I] } as Function from ALTCAT_2:sch 1();
A10:
dom f0 = ElementaryInstructions F1()
rng f0 c= F2()
then reconsider f0 = f0 as Function of ((ElementaryInstructions F1()) |^ 0),F2() by A2, A10, FUNCT_2:2;
A15:
S1[ 0 ]
proof
take
f0
;
( f0 = FF . 0 & ( EmptyIns F1() in (ElementaryInstructions F1()) |^ 0 implies f0 . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ 0 holds
f0 . (I1 \; I2) = F5((f0 . I1),(f0 . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F7((f0 . C),(f0 . I1),(f0 . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ 0 holds
f0 . (while (C,I)) = F6((f0 . C),(f0 . I)) ) )
thus
f0 = FF . 0
by A3;
( ( EmptyIns F1() in (ElementaryInstructions F1()) |^ 0 implies f0 . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ 0 holds
f0 . (I1 \; I2) = F5((f0 . I1),(f0 . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F7((f0 . C),(f0 . I1),(f0 . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ 0 holds
f0 . (while (C,I)) = F6((f0 . C),(f0 . I)) ) )
hence
( (
EmptyIns F1()
in (ElementaryInstructions F1()) |^ 0 implies
f0 . (EmptyIns F1()) = F3() ) & ( for
I1,
I2 being
Element of
F1() st
I1 \; I2 in (ElementaryInstructions F1()) |^ 0 holds
f0 . (I1 \; I2) = F5(
(f0 . I1),
(f0 . I2)) ) & ( for
C,
I1,
I2 being
Element of
F1() st
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F7(
(f0 . C),
(f0 . I1),
(f0 . I2)) ) & ( for
C,
I being
Element of
F1() st
while (
C,
I)
in (ElementaryInstructions F1()) |^ 0 holds
f0 . (while (C,I)) = F6(
(f0 . C),
(f0 . I)) ) )
by A2, Th49, Th51, Th52;
verum
end;
A17:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
given g being
Function of
((ElementaryInstructions F1()) |^ i),
F2()
such that A18:
g = FF . i
and A19:
(
EmptyIns F1()
in (ElementaryInstructions F1()) |^ i implies
g . (EmptyIns F1()) = F3() )
and A20:
for
I1,
I2 being
Element of
F1() st
I1 \; I2 in (ElementaryInstructions F1()) |^ i holds
g . (I1 \; I2) = F5(
(g . I1),
(g . I2))
and A21:
for
C,
I1,
I2 being
Element of
F1() st
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ i holds
g . (if-then-else (C,I1,I2)) = F7(
(g . C),
(g . I1),
(g . I2))
and A22:
for
C,
I being
Element of
F1() st
while (
C,
I)
in (ElementaryInstructions F1()) |^ i holds
g . (while (C,I)) = F6(
(g . C),
(g . I))
;
S1[i + 1]
set h =
FF . (i + 1);
A23:
i < i + 1
by NAT_1:13;
A24:
FF . (i + 1) = H4(
i,
g)
by A4, A18;
A25:
dom g = (ElementaryInstructions F1()) |^ i
by FUNCT_2:def 1;
A26:
(ElementaryInstructions F1()) |^ i c= (ElementaryInstructions F1()) |^ (i + 1)
by A23, Th21;
A27:
now for x being set holds
( not x in FF . (i + 1) or x in g or x in {[(EmptyIns F1()),F3()]} or x in H1(i,g) or x in H2(i,g) or x in H3(i,g) )let x be
set ;
( not x in FF . (i + 1) or x in g or x in {[(EmptyIns F1()),F3()]} or x in H1(i,g) or x in H2(i,g) or x in H3(i,g) )assume
x in FF . (i + 1)
;
( x in g or x in {[(EmptyIns F1()),F3()]} or x in H1(i,g) or x in H2(i,g) or x in H3(i,g) )then
(
x in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g) or
x in H3(
i,
g) )
by A24, XBOOLE_0:def 3;
then
(
x in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g) or
x in H2(
i,
g) or
x in H3(
i,
g) )
by XBOOLE_0:def 3;
then
(
x in g \/ {[(EmptyIns F1()),F3()]} or
x in H1(
i,
g) or
x in H2(
i,
g) or
x in H3(
i,
g) )
by XBOOLE_0:def 3;
hence
(
x in g or
x in {[(EmptyIns F1()),F3()]} or
x in H1(
i,
g) or
x in H2(
i,
g) or
x in H3(
i,
g) )
by XBOOLE_0:def 3;
verum end;
FF . (i + 1) is
Relation-like
proof
let x be
object ;
RELAT_1:def 1 ( x nin FF . (i + 1) or ex b1, b2 being object st x = [b1,b2] )
assume
x in FF . (i + 1)
;
ex b1, b2 being object st x = [b1,b2]
then
(
x in g or
x in {[(EmptyIns F1()),F3()]} or
x in H1(
i,
g) or
x in H2(
i,
g) or
x in H3(
i,
g) )
by A27;
then
( ex
a,
b being
object st
x = [a,b] or
x = [(EmptyIns F1()),F3()] or ex
I1,
I2 being
Element of
F1() ex
fI1,
fI2 being
Element of
F2() st
(
x = [(I1 \; I2),F5(fI1,fI2)] &
I1 in (ElementaryInstructions F1()) |^ i &
I2 in (ElementaryInstructions F1()) |^ i &
[I1,fI1] in g &
[I2,fI2] in g ) or ex
C,
I1,
I2 being
Element of
F1() ex
a,
b,
c being
Element of
F2() st
(
x = [(if-then-else (C,I1,I2)),F7(a,b,c)] &
C in (ElementaryInstructions F1()) |^ i &
I1 in (ElementaryInstructions F1()) |^ i &
I2 in (ElementaryInstructions F1()) |^ i &
[C,a] in g &
[I1,b] in g &
[I2,c] in g ) or ex
C,
I being
Element of
F1() ex
a,
b being
Element of
F2() st
(
x = [(while (C,I)),F6(a,b)] &
C in (ElementaryInstructions F1()) |^ i &
I in (ElementaryInstructions F1()) |^ i &
[C,a] in g &
[I,b] in g ) )
by RELAT_1:def 1;
hence
ex
b1,
b2 being
object st
x = [b1,b2]
;
verum
end;
then reconsider h =
FF . (i + 1) as
Relation ;
h is
Function-like
proof
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( [x,y1] nin h or [x,y2] nin h or y1 = y2 )
set x1 =
[x,y1];
set x2 =
[x,y2];
assume A28:
[x,y1] in h
;
( [x,y2] nin h or y1 = y2 )
assume A29:
[x,y2] in h
;
y1 = y2
per cases
( [x,y1] in g or [x,y1] in {[(EmptyIns F1()),F3()]} or [x,y1] in H1(i,g) or [x,y1] in H2(i,g) or [x,y1] in H3(i,g) )
by A27, A28;
suppose A30:
[x,y1] in g
;
y1 = y2then A31:
x in dom g
by FUNCT_1:1;
A32:
y1 = g . x
by A30, FUNCT_1:1;
per cases
( [x,y2] in g or [x,y2] in {[(EmptyIns F1()),F3()]} or [x,y2] in H1(i,g) or [x,y2] in H2(i,g) or [x,y2] in H3(i,g) )
by A27, A29;
suppose
[x,y2] in H1(
i,
g)
;
y1 = y2then consider J1,
J2 being
Element of
F1(),
gJ1,
gJ2 being
Element of
F2()
such that A34:
[x,y2] = [(J1 \; J2),F5(gJ1,gJ2)]
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and A35:
[J1,gJ1] in g
and A36:
[J2,gJ2] in g
;
A37:
x = J1 \; J2
by A34, XTUPLE_0:1;
A38:
y2 = F5(
gJ1,
gJ2)
by A34, XTUPLE_0:1;
A39:
g . J1 = gJ1
by A35, FUNCT_1:1;
g . J2 = gJ2
by A36, FUNCT_1:1;
hence
y1 = y2
by A20, A31, A32, A37, A38, A39;
verum end; suppose
[x,y2] in H2(
i,
g)
;
y1 = y2then consider D,
J1,
J2 being
Element of
F1(),
a,
b,
c being
Element of
F2()
such that A40:
[x,y2] = [(if-then-else (D,J1,J2)),F7(a,b,c)]
and
D in (ElementaryInstructions F1()) |^ i
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and A41:
[D,a] in g
and A42:
[J1,b] in g
and A43:
[J2,c] in g
;
A44:
x = if-then-else (
D,
J1,
J2)
by A40, XTUPLE_0:1;
A45:
y2 = F7(
a,
b,
c)
by A40, XTUPLE_0:1;
A46:
g . D = a
by A41, FUNCT_1:1;
A47:
g . J1 = b
by A42, FUNCT_1:1;
g . J2 = c
by A43, FUNCT_1:1;
hence
y1 = y2
by A21, A31, A32, A44, A45, A46, A47;
verum end; suppose
[x,y2] in H3(
i,
g)
;
y1 = y2then consider D,
J being
Element of
F1(),
a,
b being
Element of
F2()
such that A48:
[x,y2] = [(while (D,J)),F6(a,b)]
and
D in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and A49:
[D,a] in g
and A50:
[J,b] in g
;
A51:
x = while (
D,
J)
by A48, XTUPLE_0:1;
A52:
y2 = F6(
a,
b)
by A48, XTUPLE_0:1;
A53:
g . D = a
by A49, FUNCT_1:1;
g . J = b
by A50, FUNCT_1:1;
hence
y1 = y2
by A22, A31, A32, A51, A52, A53;
verum end; end; end; suppose
[x,y1] in {[(EmptyIns F1()),F3()]}
;
y1 = y2then A54:
[x,y1] = [(EmptyIns F1()),F3()]
by TARSKI:def 1;
then A55:
x = EmptyIns F1()
by XTUPLE_0:1;
A56:
y1 = F3()
by A54, XTUPLE_0:1;
per cases
( [x,y2] in g or [x,y2] in {[(EmptyIns F1()),F3()]} or [x,y2] in H1(i,g) or [x,y2] in H2(i,g) or [x,y2] in H3(i,g) )
by A27, A29;
suppose
[x,y2] in H1(
i,
g)
;
y1 = y2then consider J1,
J2 being
Element of
F1(),
a,
b being
Element of
F2()
such that A58:
[x,y2] = [(J1 \; J2),F5(a,b)]
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[J1,a] in g
and
[J2,b] in g
;
x = J1 \; J2
by A58, XTUPLE_0:1;
hence
y1 = y2
by A55, Th72;
verum end; suppose
[x,y2] in H2(
i,
g)
;
y1 = y2then consider D,
J1,
J2 being
Element of
F1(),
a,
b,
c being
Element of
F2()
such that A59:
[x,y2] = [(if-then-else (D,J1,J2)),F7(a,b,c)]
and
D in (ElementaryInstructions F1()) |^ i
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J1,b] in g
and
[J2,c] in g
;
x = if-then-else (
D,
J1,
J2)
by A59, XTUPLE_0:1;
hence
y1 = y2
by A55, Def24;
verum end; suppose
[x,y2] in H3(
i,
g)
;
y1 = y2then consider D,
J being
Element of
F1(),
a,
b being
Element of
F2()
such that A60:
[x,y2] = [(while (D,J)),F6(a,b)]
and
D in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J,b] in g
;
x = while (
D,
J)
by A60, XTUPLE_0:1;
hence
y1 = y2
by A55, Def24;
verum end; end; end; suppose
[x,y1] in H1(
i,
g)
;
y1 = y2then consider I1,
I2 being
Element of
F1(),
gI1,
gI2 being
Element of
F2()
such that A61:
[x,y1] = [(I1 \; I2),F5(gI1,gI2)]
and
I1 in (ElementaryInstructions F1()) |^ i
and
I2 in (ElementaryInstructions F1()) |^ i
and A62:
[I1,gI1] in g
and A63:
[I2,gI2] in g
;
A64:
x = I1 \; I2
by A61, XTUPLE_0:1;
A65:
y1 = F5(
gI1,
gI2)
by A61, XTUPLE_0:1;
A66:
g . I1 = gI1
by A62, FUNCT_1:1;
A67:
g . I2 = gI2
by A63, FUNCT_1:1;
per cases
( [x,y2] in g or [x,y2] in {[(EmptyIns F1()),F3()]} or [x,y2] in H1(i,g) or [x,y2] in H2(i,g) or [x,y2] in H3(i,g) )
by A27, A29;
suppose
[x,y2] in H1(
i,
g)
;
y1 = y2then consider J1,
J2 being
Element of
F1(),
a,
b being
Element of
F2()
such that A70:
[x,y2] = [(J1 \; J2),F5(a,b)]
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and A71:
[J1,a] in g
and A72:
[J2,b] in g
;
A73:
x = J1 \; J2
by A70, XTUPLE_0:1;
A74:
y2 = F5(
a,
b)
by A70, XTUPLE_0:1;
A75:
g . J1 = a
by A71, FUNCT_1:1;
A76:
g . J2 = b
by A72, FUNCT_1:1;
I1 = J1
by A64, A73, Th73;
hence
y1 = y2
by A64, A65, A66, A67, A73, A74, A75, A76, Th73;
verum end; suppose
[x,y2] in H2(
i,
g)
;
y1 = y2then consider D,
J1,
J2 being
Element of
F1(),
a,
b,
c being
Element of
F2()
such that A77:
[x,y2] = [(if-then-else (D,J1,J2)),F7(a,b,c)]
and
D in (ElementaryInstructions F1()) |^ i
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J1,b] in g
and
[J2,c] in g
;
x = if-then-else (
D,
J1,
J2)
by A77, XTUPLE_0:1;
hence
y1 = y2
by A64, Th73;
verum end; suppose
[x,y2] in H3(
i,
g)
;
y1 = y2then consider D,
J being
Element of
F1(),
a,
b being
Element of
F2()
such that A78:
[x,y2] = [(while (D,J)),F6(a,b)]
and
D in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J,b] in g
;
x = while (
D,
J)
by A78, XTUPLE_0:1;
hence
y1 = y2
by A64, Th73;
verum end; end; end; suppose
[x,y1] in H2(
i,
g)
;
y1 = y2then consider C,
I1,
I2 being
Element of
F1(),
gC,
gI1,
gI2 being
Element of
F2()
such that A79:
[x,y1] = [(if-then-else (C,I1,I2)),F7(gC,gI1,gI2)]
and
C in (ElementaryInstructions F1()) |^ i
and
I1 in (ElementaryInstructions F1()) |^ i
and
I2 in (ElementaryInstructions F1()) |^ i
and A80:
[C,gC] in g
and A81:
[I1,gI1] in g
and A82:
[I2,gI2] in g
;
A83:
x = if-then-else (
C,
I1,
I2)
by A79, XTUPLE_0:1;
A84:
y1 = F7(
gC,
gI1,
gI2)
by A79, XTUPLE_0:1;
A85:
g . I1 = gI1
by A81, FUNCT_1:1;
A86:
g . I2 = gI2
by A82, FUNCT_1:1;
A87:
g . C = gC
by A80, FUNCT_1:1;
per cases
( [x,y2] in g or [x,y2] in {[(EmptyIns F1()),F3()]} or [x,y2] in H1(i,g) or [x,y2] in H2(i,g) or [x,y2] in H3(i,g) )
by A27, A29;
suppose
[x,y2] in H1(
i,
g)
;
y1 = y2then consider J1,
J2 being
Element of
F1(),
a,
b being
Element of
F2()
such that A90:
[x,y2] = [(J1 \; J2),F5(a,b)]
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[J1,a] in g
and
[J2,b] in g
;
x = J1 \; J2
by A90, XTUPLE_0:1;
hence
y1 = y2
by A83, Th73;
verum end; suppose
[x,y2] in H2(
i,
g)
;
y1 = y2then consider D,
J1,
J2 being
Element of
F1(),
a,
b,
c being
Element of
F2()
such that A91:
[x,y2] = [(if-then-else (D,J1,J2)),F7(a,b,c)]
and
D in (ElementaryInstructions F1()) |^ i
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and A92:
[D,a] in g
and A93:
[J1,b] in g
and A94:
[J2,c] in g
;
A95:
x = if-then-else (
D,
J1,
J2)
by A91, XTUPLE_0:1;
A96:
y2 = F7(
a,
b,
c)
by A91, XTUPLE_0:1;
A97:
g . D = a
by A92, FUNCT_1:1;
A98:
g . J1 = b
by A93, FUNCT_1:1;
A99:
g . J2 = c
by A94, FUNCT_1:1;
A100:
C = D
by A83, A95, Th74;
I1 = J1
by A83, A95, Th74;
hence
y1 = y2
by A83, A84, A85, A86, A87, A95, A96, A97, A98, A99, A100, Th74;
verum end; suppose
[x,y2] in H3(
i,
g)
;
y1 = y2then consider D,
J being
Element of
F1(),
a,
b being
Element of
F2()
such that A101:
[x,y2] = [(while (D,J)),F6(a,b)]
and
D in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J,b] in g
;
x = while (
D,
J)
by A101, XTUPLE_0:1;
hence
y1 = y2
by A83, Th74;
verum end; end; end; suppose
[x,y1] in H3(
i,
g)
;
y1 = y2then consider C,
I being
Element of
F1(),
gC,
gI being
Element of
F2()
such that A102:
[x,y1] = [(while (C,I)),F6(gC,gI)]
and
C in (ElementaryInstructions F1()) |^ i
and
I in (ElementaryInstructions F1()) |^ i
and A103:
[C,gC] in g
and A104:
[I,gI] in g
;
A105:
x = while (
C,
I)
by A102, XTUPLE_0:1;
A106:
y1 = F6(
gC,
gI)
by A102, XTUPLE_0:1;
A107:
g . C = gC
by A103, FUNCT_1:1;
A108:
g . I = gI
by A104, FUNCT_1:1;
per cases
( [x,y2] in g or [x,y2] in {[(EmptyIns F1()),F3()]} or [x,y2] in H1(i,g) or [x,y2] in H2(i,g) or [x,y2] in H3(i,g) )
by A27, A29;
suppose
[x,y2] in H1(
i,
g)
;
y1 = y2then consider J1,
J2 being
Element of
F1(),
a,
b being
Element of
F2()
such that A111:
[x,y2] = [(J1 \; J2),F5(a,b)]
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[J1,a] in g
and
[J2,b] in g
;
x = J1 \; J2
by A111, XTUPLE_0:1;
hence
y1 = y2
by A105, Th73;
verum end; suppose
[x,y2] in H2(
i,
g)
;
y1 = y2then consider D,
J1,
J2 being
Element of
F1(),
a,
b,
c being
Element of
F2()
such that A112:
[x,y2] = [(if-then-else (D,J1,J2)),F7(a,b,c)]
and
D in (ElementaryInstructions F1()) |^ i
and
J1 in (ElementaryInstructions F1()) |^ i
and
J2 in (ElementaryInstructions F1()) |^ i
and
[D,a] in g
and
[J1,b] in g
and
[J2,c] in g
;
x = if-then-else (
D,
J1,
J2)
by A112, XTUPLE_0:1;
hence
y1 = y2
by A105, Th74;
verum end; suppose
[x,y2] in H3(
i,
g)
;
y1 = y2then consider D,
J being
Element of
F1(),
a,
b being
Element of
F2()
such that A113:
[x,y2] = [(while (D,J)),F6(a,b)]
and
D in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and A114:
[D,a] in g
and A115:
[J,b] in g
;
A116:
x = while (
D,
J)
by A113, XTUPLE_0:1;
A117:
y2 = F6(
a,
b)
by A113, XTUPLE_0:1;
A118:
g . D = a
by A114, FUNCT_1:1;
A119:
g . J = b
by A115, FUNCT_1:1;
D = C
by A105, A116, Th75;
hence
y1 = y2
by A105, A106, A107, A108, A116, A117, A118, A119, Th75;
verum end; end; end; end;
end;
then reconsider h =
h as
Function ;
A120:
dom h = (ElementaryInstructions F1()) |^ (i + 1)
proof
thus
dom h c= (ElementaryInstructions F1()) |^ (i + 1)
XBOOLE_0:def 10 (ElementaryInstructions F1()) |^ (i + 1) c= dom hproof
let a be
object ;
TARSKI:def 3 ( a nin dom h or not a nin (ElementaryInstructions F1()) |^ (i + 1) )
set ah =
[a,(h . a)];
assume
a in dom h
;
not a nin (ElementaryInstructions F1()) |^ (i + 1)
then A121:
[a,(h . a)] in h
by FUNCT_1:def 2;
per cases
( [a,(h . a)] in g or [a,(h . a)] in {[(EmptyIns F1()),F3()]} or [a,(h . a)] in H1(i,g) or [a,(h . a)] in H2(i,g) or [a,(h . a)] in H3(i,g) )
by A27, A121;
suppose
[a,(h . a)] in H1(
i,
g)
;
not a nin (ElementaryInstructions F1()) |^ (i + 1)then consider I,
J being
Element of
F1(),
e,
b being
Element of
F2()
such that A122:
[a,(h . a)] = [(I \; J),F5(e,b)]
and A123:
I in (ElementaryInstructions F1()) |^ i
and A124:
J in (ElementaryInstructions F1()) |^ i
and
[I,e] in g
and
[J,b] in g
;
a = I \; J
by A122, XTUPLE_0:1;
hence
not
a nin (ElementaryInstructions F1()) |^ (i + 1)
by A123, A124, Th76;
verum end; suppose
[a,(h . a)] in H2(
i,
g)
;
not a nin (ElementaryInstructions F1()) |^ (i + 1)then consider C,
I,
J being
Element of
F1(),
e,
b,
c being
Element of
F2()
such that A125:
[a,(h . a)] = [(if-then-else (C,I,J)),F7(e,b,c)]
and A126:
C in (ElementaryInstructions F1()) |^ i
and A127:
I in (ElementaryInstructions F1()) |^ i
and A128:
J in (ElementaryInstructions F1()) |^ i
and
[C,e] in g
and
[I,b] in g
and
[J,c] in g
;
a = if-then-else (
C,
I,
J)
by A125, XTUPLE_0:1;
hence
not
a nin (ElementaryInstructions F1()) |^ (i + 1)
by A126, A127, A128, Th76;
verum end; suppose
[a,(h . a)] in H3(
i,
g)
;
not a nin (ElementaryInstructions F1()) |^ (i + 1)then consider I,
J being
Element of
F1(),
e,
b being
Element of
F2()
such that A129:
[a,(h . a)] = [(while (I,J)),F6(e,b)]
and A130:
I in (ElementaryInstructions F1()) |^ i
and A131:
J in (ElementaryInstructions F1()) |^ i
and
[I,e] in g
and
[J,b] in g
;
a = while (
I,
J)
by A129, XTUPLE_0:1;
hence
not
a nin (ElementaryInstructions F1()) |^ (i + 1)
by A130, A131, Th76;
verum end; end;
end;
let x be
object ;
TARSKI:def 3 ( x nin (ElementaryInstructions F1()) |^ (i + 1) or not x nin dom h )
assume A132:
x in (ElementaryInstructions F1()) |^ (i + 1)
;
not x nin dom h
per cases
( x in (ElementaryInstructions F1()) |^ i or x = EmptyIns F1() or ex I1, I2 being Element of F1() st
( x = I1 \; I2 & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i ) or ex C, I1, I2 being Element of F1() st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions F1()) |^ i & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i ) or ex C, I being Element of F1() st
( x = while (C,I) & C in (ElementaryInstructions F1()) |^ i & I in (ElementaryInstructions F1()) |^ i ) )
by A132, Th77;
suppose
x in (ElementaryInstructions F1()) |^ i
;
not x nin dom hthen
[x,(g . x)] in g
by A25, FUNCT_1:def 2;
then
[x,(g . x)] in g \/ {[(EmptyIns F1()),F3()]}
by XBOOLE_0:def 3;
then
[x,(g . x)] in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g)
by XBOOLE_0:def 3;
then
[x,(g . x)] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[x,(g . x)] in h
by A24, XBOOLE_0:def 3;
hence
not
x nin dom h
by XTUPLE_0:def 12;
verum end; suppose
x = EmptyIns F1()
;
not x nin dom hthen
[x,F3()] in {[(EmptyIns F1()),F3()]}
by TARSKI:def 1;
then
[x,F3()] in g \/ {[(EmptyIns F1()),F3()]}
by XBOOLE_0:def 3;
then
[x,F3()] in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g)
by XBOOLE_0:def 3;
then
[x,F3()] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[x,F3()] in h
by A24, XBOOLE_0:def 3;
hence
not
x nin dom h
by XTUPLE_0:def 12;
verum end; suppose
ex
I1,
I2 being
Element of
F1() st
(
x = I1 \; I2 &
I1 in (ElementaryInstructions F1()) |^ i &
I2 in (ElementaryInstructions F1()) |^ i )
;
not x nin dom hthen consider I1,
I2 being
Element of
F1()
such that A133:
x = I1 \; I2
and A134:
I1 in (ElementaryInstructions F1()) |^ i
and A135:
I2 in (ElementaryInstructions F1()) |^ i
;
reconsider a =
g . I1,
b =
g . I2 as
Element of
F2()
by A134, A135, FUNCT_2:5;
A136:
[I1,a] in g
by A25, A134, FUNCT_1:def 2;
[I2,b] in g
by A25, A135, FUNCT_1:def 2;
then
[x,F5(a,b)] in H1(
i,
g)
by A133, A134, A135, A136;
then
[x,F5(a,b)] in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g)
by XBOOLE_0:def 3;
then
[x,F5(a,b)] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[x,F5(a,b)] in h
by A24, XBOOLE_0:def 3;
hence
not
x nin dom h
by XTUPLE_0:def 12;
verum end; suppose
ex
C,
I1,
I2 being
Element of
F1() st
(
x = if-then-else (
C,
I1,
I2) &
C in (ElementaryInstructions F1()) |^ i &
I1 in (ElementaryInstructions F1()) |^ i &
I2 in (ElementaryInstructions F1()) |^ i )
;
not x nin dom hthen consider C,
I1,
I2 being
Element of
F1()
such that A137:
x = if-then-else (
C,
I1,
I2)
and A138:
C in (ElementaryInstructions F1()) |^ i
and A139:
I1 in (ElementaryInstructions F1()) |^ i
and A140:
I2 in (ElementaryInstructions F1()) |^ i
;
reconsider a =
g . I1,
b =
g . I2,
c =
g . C as
Element of
F2()
by A138, A139, A140, FUNCT_2:5;
A141:
[I1,a] in g
by A25, A139, FUNCT_1:def 2;
A142:
[I2,b] in g
by A25, A140, FUNCT_1:def 2;
[C,c] in g
by A25, A138, FUNCT_1:def 2;
then
[x,F7(c,a,b)] in H2(
i,
g)
by A137, A138, A139, A140, A141, A142;
then
[x,F7(c,a,b)] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[x,F7(c,a,b)] in h
by A24, XBOOLE_0:def 3;
hence
not
x nin dom h
by XTUPLE_0:def 12;
verum end; suppose
ex
C,
I being
Element of
F1() st
(
x = while (
C,
I) &
C in (ElementaryInstructions F1()) |^ i &
I in (ElementaryInstructions F1()) |^ i )
;
not x nin dom hthen consider C,
I being
Element of
F1()
such that A143:
x = while (
C,
I)
and A144:
C in (ElementaryInstructions F1()) |^ i
and A145:
I in (ElementaryInstructions F1()) |^ i
;
reconsider a =
g . C,
b =
g . I as
Element of
F2()
by A144, A145, FUNCT_2:5;
A146:
[C,a] in g
by A25, A144, FUNCT_1:def 2;
[I,b] in g
by A25, A145, FUNCT_1:def 2;
then
[x,F6(a,b)] in H3(
i,
g)
by A143, A144, A145, A146;
then
[x,F6(a,b)] in h
by A24, XBOOLE_0:def 3;
hence
not
x nin dom h
by XTUPLE_0:def 12;
verum end; end;
end;
rng h c= F2()
proof
let a be
object ;
TARSKI:def 3 ( a nin rng h or not a nin F2() )
assume
a in rng h
;
not a nin F2()
then consider x being
object such that A147:
[x,a] in h
by XTUPLE_0:def 13;
set ah =
[x,a];
per cases
( [x,a] in g or [x,a] in {[(EmptyIns F1()),F3()]} or [x,a] in H1(i,g) or [x,a] in H2(i,g) or [x,a] in H3(i,g) )
by A27, A147;
suppose
[x,a] in H1(
i,
g)
;
not a nin F2()then consider I,
J being
Element of
F1(),
e,
b being
Element of
F2()
such that A148:
[x,a] = [(I \; J),F5(e,b)]
and
I in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[I,e] in g
and
[J,b] in g
;
a = F5(
e,
b)
by A148, XTUPLE_0:1;
hence
not
a nin F2()
;
verum end; suppose
[x,a] in H2(
i,
g)
;
not a nin F2()then consider C,
I,
J being
Element of
F1(),
e,
b,
c being
Element of
F2()
such that A149:
[x,a] = [(if-then-else (C,I,J)),F7(e,b,c)]
and
C in (ElementaryInstructions F1()) |^ i
and
I in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[C,e] in g
and
[I,b] in g
and
[J,c] in g
;
a = F7(
e,
b,
c)
by A149, XTUPLE_0:1;
hence
not
a nin F2()
;
verum end; suppose
[x,a] in H3(
i,
g)
;
not a nin F2()then consider I,
J being
Element of
F1(),
e,
b being
Element of
F2()
such that A150:
[x,a] = [(while (I,J)),F6(e,b)]
and
I in (ElementaryInstructions F1()) |^ i
and
J in (ElementaryInstructions F1()) |^ i
and
[I,e] in g
and
[J,b] in g
;
a = F6(
e,
b)
by A150, XTUPLE_0:1;
hence
not
a nin F2()
;
verum end; end;
end;
then reconsider h =
h as
Function of
((ElementaryInstructions F1()) |^ (i + 1)),
F2()
by A120, FUNCT_2:2;
h =
((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ (H2(i,g) \/ H3(i,g))
by A24, XBOOLE_1:4
.=
(g \/ {[(EmptyIns F1()),F3()]}) \/ (H1(i,g) \/ (H2(i,g) \/ H3(i,g)))
by XBOOLE_1:4
.=
g \/ ({[(EmptyIns F1()),F3()]} \/ (H1(i,g) \/ (H2(i,g) \/ H3(i,g))))
by XBOOLE_1:4
;
then A151:
g c= h
by XBOOLE_1:7;
take
h
;
( h = FF . (i + 1) & ( EmptyIns F1() in (ElementaryInstructions F1()) |^ (i + 1) implies h . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (I1 \; I2) = F5((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (while (C,I)) = F6((h . C),(h . I)) ) )
thus
h = FF . (i + 1)
;
( ( EmptyIns F1() in (ElementaryInstructions F1()) |^ (i + 1) implies h . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (I1 \; I2) = F5((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (while (C,I)) = F6((h . C),(h . I)) ) )
hereby ( ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (I1 \; I2) = F5((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (while (C,I)) = F6((h . C),(h . I)) ) )
set x =
EmptyIns F1();
assume
EmptyIns F1()
in (ElementaryInstructions F1()) |^ (i + 1)
;
h . (EmptyIns F1()) = F3()
[(EmptyIns F1()),F3()] in {[(EmptyIns F1()),F3()]}
by TARSKI:def 1;
then
[(EmptyIns F1()),F3()] in g \/ {[(EmptyIns F1()),F3()]}
by XBOOLE_0:def 3;
then
[(EmptyIns F1()),F3()] in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g)
by XBOOLE_0:def 3;
then
[(EmptyIns F1()),F3()] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[(EmptyIns F1()),F3()] in h
by A24, XBOOLE_0:def 3;
hence
h . (EmptyIns F1()) = F3()
by FUNCT_1:1;
verum
end;
hereby ( ( for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (while (C,I)) = F6((h . C),(h . I)) ) )
let I1,
I2 be
Element of
F1();
( I1 \; I2 in (ElementaryInstructions F1()) |^ (i + 1) implies h . (I1 \; I2) = F5((h . I1),(h . I2)) )set x =
I1 \; I2;
set y =
F5(
(h . I1),
(h . I2));
assume
I1 \; I2 in (ElementaryInstructions F1()) |^ (i + 1)
;
h . (I1 \; I2) = F5((h . I1),(h . I2))then A152:
ex
i0 being
Nat st
(
i + 1
= i0 + 1 &
I1 in (ElementaryInstructions F1()) |^ i0 &
I2 in (ElementaryInstructions F1()) |^ i0 )
by Th88;
then reconsider gI1 =
g . I1,
gI2 =
g . I2 as
Element of
F2()
by FUNCT_2:5;
A153:
[I1,gI1] in g
by A25, A152, FUNCT_1:def 2;
A154:
[I2,gI2] in g
by A25, A152, FUNCT_1:def 2;
A155:
g . I1 = h . I1
by A151, A153, FUNCT_1:1;
g . I2 = h . I2
by A151, A154, FUNCT_1:1;
then
[(I1 \; I2),F5((h . I1),(h . I2))] in H1(
i,
g)
by A152, A153, A154, A155;
then
[(I1 \; I2),F5((h . I1),(h . I2))] in (g \/ {[(EmptyIns F1()),F3()]}) \/ H1(
i,
g)
by XBOOLE_0:def 3;
then
[(I1 \; I2),F5((h . I1),(h . I2))] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[(I1 \; I2),F5((h . I1),(h . I2))] in h
by A24, XBOOLE_0:def 3;
hence
h . (I1 \; I2) = F5(
(h . I1),
(h . I2))
by FUNCT_1:1;
verum
end;
hereby for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) holds
h . (while (C,I)) = F6((h . C),(h . I))
let C,
I1,
I2 be
Element of
F1();
( if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ (i + 1) implies h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2)) )set x =
if-then-else (
C,
I1,
I2);
set y =
F7(
(h . C),
(h . I1),
(h . I2));
assume
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ (i + 1)
;
h . (if-then-else (C,I1,I2)) = F7((h . C),(h . I1),(h . I2))then A156:
ex
i0 being
Nat st
(
i + 1
= i0 + 1 &
C in (ElementaryInstructions F1()) |^ i0 &
I1 in (ElementaryInstructions F1()) |^ i0 &
I2 in (ElementaryInstructions F1()) |^ i0 )
by Th89;
then reconsider gC =
g . C,
gI1 =
g . I1,
gI2 =
g . I2 as
Element of
F2()
by FUNCT_2:5;
A157:
[C,gC] in g
by A25, A156, FUNCT_1:def 2;
A158:
[I1,gI1] in g
by A25, A156, FUNCT_1:def 2;
A159:
[I2,gI2] in g
by A25, A156, FUNCT_1:def 2;
A160:
g . C = h . C
by A151, A157, FUNCT_1:1;
A161:
g . I1 = h . I1
by A151, A158, FUNCT_1:1;
g . I2 = h . I2
by A151, A159, FUNCT_1:1;
then
[(if-then-else (C,I1,I2)),F7((h . C),(h . I1),(h . I2))] in H2(
i,
g)
by A156, A157, A158, A159, A160, A161;
then
[(if-then-else (C,I1,I2)),F7((h . C),(h . I1),(h . I2))] in ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ H2(
i,
g)
by XBOOLE_0:def 3;
then
[(if-then-else (C,I1,I2)),F7((h . C),(h . I1),(h . I2))] in h
by A24, XBOOLE_0:def 3;
hence
h . (if-then-else (C,I1,I2)) = F7(
(h . C),
(h . I1),
(h . I2))
by FUNCT_1:1;
verum
end;
let C,
I be
Element of
F1();
( while (C,I) in (ElementaryInstructions F1()) |^ (i + 1) implies h . (while (C,I)) = F6((h . C),(h . I)) )
set x =
while (
C,
I);
set y =
F6(
(h . C),
(h . I));
assume
while (
C,
I)
in (ElementaryInstructions F1()) |^ (i + 1)
;
h . (while (C,I)) = F6((h . C),(h . I))
then A162:
ex
i0 being
Nat st
(
i + 1
= i0 + 1 &
C in (ElementaryInstructions F1()) |^ i0 &
I in (ElementaryInstructions F1()) |^ i0 )
by Th90;
then reconsider gC =
g . C,
gI =
g . I as
Element of
F2()
by FUNCT_2:5;
A163:
[C,gC] in g
by A25, A162, FUNCT_1:def 2;
A164:
[I,gI] in g
by A25, A162, FUNCT_1:def 2;
A165:
g . C = h . C
by A151, A163, FUNCT_1:1;
g . I = h . I
by A151, A164, FUNCT_1:1;
then
[(while (C,I)),F6((h . C),(h . I))] in H3(
i,
g)
by A162, A163, A164, A165;
then
[(while (C,I)),F6((h . C),(h . I))] in h
by A24, XBOOLE_0:def 3;
hence
h . (while (C,I)) = F6(
(h . C),
(h . I))
by FUNCT_1:1;
verum
end;
A166:
for i being Nat holds S1[i]
from NAT_1:sch 2(A15, A17);
( Union FF is Relation-like & Union FF is Function-like )
proof
let x,
y1,
y2 be
object ;
FUNCT_1:def 1 ( [x,y1] nin Union FF or [x,y2] nin Union FF or y1 = y2 )
assume
[x,y1] in Union FF
;
( [x,y2] nin Union FF or y1 = y2 )
then consider n1 being
object such that A169:
n1 in dom FF
and A170:
[x,y1] in FF . n1
by CARD_5:2;
assume
[x,y2] in Union FF
;
y1 = y2
then consider n2 being
object such that A171:
n2 in dom FF
and A172:
[x,y2] in FF . n2
by CARD_5:2;
reconsider n1 =
n1,
n2 =
n2 as
Element of
NAT by A3, A169, A171;
(
n1 <= n2 or
n2 <= n1 )
;
then
(
FF . n1 c= FF . n2 or
FF . n2 c= FF . n1 )
by A5;
then
( (
[x,y1] in FF . n2 &
S1[
n2] ) or (
[x,y2] in FF . n1 &
S1[
n1] ) )
by A166, A170, A172;
hence
y1 = y2
by A170, A172, FUNCT_1:def 1;
verum
end;
then reconsider f = Union FF as Function ;
A173:
dom f = the carrier of F1()
rng f c= F2()
then reconsider f = f as Function of the carrier of F1(),F2() by A173, FUNCT_2:2;
take
f
; ( ( for I being Element of F1() st I in ElementaryInstructions F1() holds
f . I = F4(I) ) & f . (EmptyIns F1()) = F3() & ( for I1, I2 being Element of F1() holds f . (I1 \; I2) = F5((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I)) ) )
hereby ( f . (EmptyIns F1()) = F3() & ( for I1, I2 being Element of F1() holds f . (I1 \; I2) = F5((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I)) ) )
end;
consider n0 being Nat such that
A186:
EmptyIns F1() in (ElementaryInstructions F1()) |^ n0
by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A187:
g0 = FF . n0
and
A188:
( EmptyIns F1() in (ElementaryInstructions F1()) |^ n0 implies g0 . (EmptyIns F1()) = F3() )
and
for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ n0 holds
g0 . (I1 \; I2) = F5((g0 . I1),(g0 . I2))
and
for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F7((g0 . C),(g0 . I1),(g0 . I2))
and
for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ n0 holds
g0 . (while (C,I)) = F6((g0 . C),(g0 . I))
by A166;
dom g0 = (ElementaryInstructions F1()) |^ n0
by FUNCT_2:def 1;
then
[(EmptyIns F1()),F3()] in g0
by A186, A188, FUNCT_1:def 2;
then
[(EmptyIns F1()),F3()] in f
by A3, A187, CARD_5:2;
hence
f . (EmptyIns F1()) = F3()
by FUNCT_1:1; ( ( for I1, I2 being Element of F1() holds f . (I1 \; I2) = F5((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I)) ) )
hereby ( ( for C, I1, I2 being Element of F1() holds f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I)) ) )
let I1,
I2 be
Element of
F1();
f . (I1 \; I2) = F5((f . I1),(f . I2))consider n0 being
Nat such that A189:
I1 \; I2 in (ElementaryInstructions F1()) |^ n0
by Th79;
reconsider n0 =
n0 as
Element of
NAT by ORDINAL1:def 12;
consider g0 being
Function of
((ElementaryInstructions F1()) |^ n0),
F2()
such that A190:
g0 = FF . n0
and
(
EmptyIns F1()
in (ElementaryInstructions F1()) |^ n0 implies
g0 . (EmptyIns F1()) = F3() )
and A191:
for
I1,
I2 being
Element of
F1() st
I1 \; I2 in (ElementaryInstructions F1()) |^ n0 holds
g0 . (I1 \; I2) = F5(
(g0 . I1),
(g0 . I2))
and
for
C,
I1,
I2 being
Element of
F1() st
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F7(
(g0 . C),
(g0 . I1),
(g0 . I2))
and
for
C,
I being
Element of
F1() st
while (
C,
I)
in (ElementaryInstructions F1()) |^ n0 holds
g0 . (while (C,I)) = F6(
(g0 . C),
(g0 . I))
by A166;
consider i0 being
Nat such that A192:
n0 = i0 + 1
and A193:
I1 in (ElementaryInstructions F1()) |^ i0
and A194:
I2 in (ElementaryInstructions F1()) |^ i0
by A189, Th88;
n0 > i0
by A192, NAT_1:13;
then A195:
(ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0
by Th21;
A196:
dom g0 = (ElementaryInstructions F1()) |^ n0
by FUNCT_2:def 1;
A197:
g0 . I1 = f . I1
by A182, A190, A193, A195;
A198:
g0 . I2 = f . I2
by A182, A190, A194, A195;
A199:
[(I1 \; I2),(g0 . (I1 \; I2))] in g0
by A189, A196, FUNCT_1:1;
g0 . (I1 \; I2) = F5(
(f . I1),
(f . I2))
by A189, A191, A197, A198;
then
[(I1 \; I2),F5((f . I1),(f . I2))] in f
by A3, A190, A199, CARD_5:2;
hence
f . (I1 \; I2) = F5(
(f . I1),
(f . I2))
by FUNCT_1:1;
verum
end;
hereby for C, I being Element of F1() holds f . (while (C,I)) = F6((f . C),(f . I))
let C,
I1,
I2 be
Element of
F1();
f . (if-then-else (C,I1,I2)) = F7((f . C),(f . I1),(f . I2))set IF =
if-then-else (
C,
I1,
I2);
consider n0 being
Nat such that A200:
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ n0
by Th79;
reconsider n0 =
n0 as
Element of
NAT by ORDINAL1:def 12;
consider g0 being
Function of
((ElementaryInstructions F1()) |^ n0),
F2()
such that A201:
g0 = FF . n0
and
(
EmptyIns F1()
in (ElementaryInstructions F1()) |^ n0 implies
g0 . (EmptyIns F1()) = F3() )
and
for
I1,
I2 being
Element of
F1() st
I1 \; I2 in (ElementaryInstructions F1()) |^ n0 holds
g0 . (I1 \; I2) = F5(
(g0 . I1),
(g0 . I2))
and A202:
for
C,
I1,
I2 being
Element of
F1() st
if-then-else (
C,
I1,
I2)
in (ElementaryInstructions F1()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F7(
(g0 . C),
(g0 . I1),
(g0 . I2))
and
for
C,
I being
Element of
F1() st
while (
C,
I)
in (ElementaryInstructions F1()) |^ n0 holds
g0 . (while (C,I)) = F6(
(g0 . C),
(g0 . I))
by A166;
consider i0 being
Nat such that A203:
n0 = i0 + 1
and A204:
C in (ElementaryInstructions F1()) |^ i0
and A205:
I1 in (ElementaryInstructions F1()) |^ i0
and A206:
I2 in (ElementaryInstructions F1()) |^ i0
by A200, Th89;
n0 > i0
by A203, NAT_1:13;
then A207:
(ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0
by Th21;
A208:
dom g0 = (ElementaryInstructions F1()) |^ n0
by FUNCT_2:def 1;
A209:
g0 . C = f . C
by A182, A201, A204, A207;
A210:
g0 . I1 = f . I1
by A182, A201, A205, A207;
A211:
g0 . I2 = f . I2
by A182, A201, A206, A207;
A212:
[(if-then-else (C,I1,I2)),(g0 . (if-then-else (C,I1,I2)))] in g0
by A200, A208, FUNCT_1:1;
g0 . (if-then-else (C,I1,I2)) = F7(
(f . C),
(f . I1),
(f . I2))
by A200, A202, A209, A210, A211;
then
[(if-then-else (C,I1,I2)),F7((f . C),(f . I1),(f . I2))] in f
by A3, A201, A212, CARD_5:2;
hence
f . (if-then-else (C,I1,I2)) = F7(
(f . C),
(f . I1),
(f . I2))
by FUNCT_1:1;
verum
end;
let C, I be Element of F1(); f . (while (C,I)) = F6((f . C),(f . I))
set WH = while (C,I);
consider n0 being Nat such that
A213:
while (C,I) in (ElementaryInstructions F1()) |^ n0
by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A214:
g0 = FF . n0
and
( EmptyIns F1() in (ElementaryInstructions F1()) |^ n0 implies g0 . (EmptyIns F1()) = F3() )
and
for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ n0 holds
g0 . (I1 \; I2) = F5((g0 . I1),(g0 . I2))
and
for C, I1, I2 being Element of F1() st if-then-else (C,I1,I2) in (ElementaryInstructions F1()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F7((g0 . C),(g0 . I1),(g0 . I2))
and
A215:
for C, I being Element of F1() st while (C,I) in (ElementaryInstructions F1()) |^ n0 holds
g0 . (while (C,I)) = F6((g0 . C),(g0 . I))
by A166;
consider i0 being Nat such that
A216:
n0 = i0 + 1
and
A217:
C in (ElementaryInstructions F1()) |^ i0
and
A218:
I in (ElementaryInstructions F1()) |^ i0
by A213, Th90;
n0 > i0
by A216, NAT_1:13;
then A219:
(ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0
by Th21;
A220:
dom g0 = (ElementaryInstructions F1()) |^ n0
by FUNCT_2:def 1;
A221:
g0 . C = f . C
by A182, A214, A217, A219;
A222:
g0 . I = f . I
by A182, A214, A218, A219;
A223:
[(while (C,I)),(g0 . (while (C,I)))] in g0
by A213, A220, FUNCT_1:1;
g0 . (while (C,I)) = F6((f . C),(f . I))
by A213, A215, A221, A222;
then
[(while (C,I)),F6((f . C),(f . I))] in f
by A3, A214, A223, CARD_5:2;
hence
f . (while (C,I)) = F6((f . C),(f . I))
by FUNCT_1:1; verum