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; :: thesis: ( n <= m implies FF . n c= FF . m )
assume n <= m ; :: thesis: 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 :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( 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; :: thesis: verum
end;
for i being Nat holds S1[i] from NAT_1:sch 2(A8, A9);
 hence FF . n c= FF . m by A7; :: thesis: 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()
proof
thus dom f0 c= ElementaryInstructions F1() :: according to XBOOLE_0:def 10 :: thesis: ElementaryInstructions F1() c= dom f0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin dom f0 or not x nin ElementaryInstructions F1() )
assume x in dom f0 ; :: thesis: not x nin ElementaryInstructions F1()
then [x,(f0 . x)] in f0 by FUNCT_1:def 2;
then ex I being Element of F1() st
( [x,(f0 . x)] = [I,F4(I)] & S2[I] ) ;
hence not x nin ElementaryInstructions F1() by XTUPLE_0:1; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin ElementaryInstructions F1() or not x nin dom f0 )
assume A11: x in ElementaryInstructions F1() ; :: thesis: not x nin dom f0
then reconsider I = x as Element of F1() ;
[I,F4(I)] in f0 by A11;
hence not x nin dom f0 by XTUPLE_0:def 12; :: thesis: verum
end;
rng f0 c= F2()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( y nin rng f0 or not y nin F2() )
assume y in rng f0 ; :: thesis: not y nin F2()
then consider x being object such that
A12: [x,y] in f0 by XTUPLE_0:def 13;
consider I being Element of F1() such that
A13: [x,y] = [I,F4(I)] and
A14: S2[I] by A12;
y = F4(I) by A13, XTUPLE_0:1;
hence not y nin F2() by A1, A14; :: thesis: verum
end;
then reconsider f0 = f0 as Function of ((ElementaryInstructions F1()) |^ 0),F2() by A2, A10, FUNCT_2:2;
A15: S1[ 0 ]
proof
take f0 ; :: thesis: ( 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; :: thesis: ( ( 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)) ) )
now :: thesis: for I1, I2 being Element of F1() holds I1 \; I2 nin ElementaryInstructions F1()
let I1, I2 be Element of F1(); :: thesis: I1 \; I2 nin ElementaryInstructions F1()
A16: I1 \; I2 <> I1 by Th73;
I1 \; I2 <> I2 by Th73;
hence I1 \; I2 nin ElementaryInstructions F1() by A16, Th50; :: thesis: verum
end;
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; :: thesis: verum
end;
A17: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( 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)) ; :: thesis: 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 :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( 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; :: thesis: verum
end;
FF . (i + 1) is Relation-like
proof
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( x nin FF . (i + 1) or ex b1, b2 being object st x = [b1,b2] )
assume x in FF . (i + 1) ; :: thesis: 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] ; :: thesis: verum
end;
then reconsider h = FF . (i + 1) as Relation ;
h is Function-like
proof
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( [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 ; :: thesis: ( [x,y2] nin h or y1 = y2 )
assume A29: [x,y2] in h ; :: thesis: 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 ; :: thesis: y1 = y2
then 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 g ; :: thesis: y1 = y2
hence y1 = y2 by A30, FUNCT_1:def 1; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then A33: [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then x = EmptyIns F1() by XTUPLE_0:1;
hence y1 = y2 by A19, A31, A32, A33, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y2] in H1(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H2(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H3(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
end;
end;
suppose [x,y1] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then 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 {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
hence y1 = y2 by A54, XTUPLE_0:1; :: thesis: verum
end;
suppose [x,y2] in H1(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H2(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H3(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
end;
end;
suppose [x,y1] in H1(i,g) ; :: thesis: y1 = y2
then 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 {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then x = EmptyIns F1() by XTUPLE_0:1;
hence y1 = y2 by A64, Th72; :: thesis: verum
end;
suppose [x,y2] in H1(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H2(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H3(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
end;
end;
suppose [x,y1] in H2(i,g) ; :: thesis: y1 = y2
then 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 {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then x = EmptyIns F1() by XTUPLE_0:1;
hence y1 = y2 by A83, Th72; :: thesis: verum
end;
suppose [x,y2] in H1(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H2(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H3(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
end;
end;
suppose [x,y1] in H3(i,g) ; :: thesis: y1 = y2
then 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 {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then x = EmptyIns F1() by XTUPLE_0:1;
hence y1 = y2 by A105, Th72; :: thesis: verum
end;
suppose [x,y2] in H1(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H2(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: verum
end;
suppose [x,y2] in H3(i,g) ; :: thesis: y1 = y2
then 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; :: thesis: 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) :: according to XBOOLE_0:def 10 :: thesis: (ElementaryInstructions F1()) |^ (i + 1) c= dom h
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin dom h or not a nin (ElementaryInstructions F1()) |^ (i + 1) )
set ah = [a,(h . a)];
assume a in dom h ; :: thesis: 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 {[(EmptyIns F1()),F3()]} ; :: thesis: not a nin (ElementaryInstructions F1()) |^ (i + 1)
then [a,(h . a)] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then a = EmptyIns F1() by XTUPLE_0:1;
hence not a nin (ElementaryInstructions F1()) |^ (i + 1) by Th76; :: thesis: verum
end;
suppose [a,(h . a)] in H1(i,g) ; :: thesis: 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; :: thesis: verum
end;
suppose [a,(h . a)] in H2(i,g) ; :: thesis: 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; :: thesis: verum
end;
suppose [a,(h . a)] in H3(i,g) ; :: thesis: 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; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin (ElementaryInstructions F1()) |^ (i + 1) or not x nin dom h )
assume A132: x in (ElementaryInstructions F1()) |^ (i + 1) ; :: thesis: 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 ; :: thesis: not x nin dom h
then [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; :: thesis: verum
end;
suppose x = EmptyIns F1() ; :: thesis: not x nin dom h
then [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; :: thesis: verum
end;
suppose ex I1, I2 being Element of F1() st
( x = I1 \; I2 & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i ) ; :: thesis: not x nin dom h
then 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; :: thesis: 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 ) ; :: thesis: not x nin dom h
then 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; :: thesis: 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 ) ; :: thesis: not x nin dom h
then 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; :: thesis: verum
end;
end;
end;
rng h c= F2()
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin rng h or not a nin F2() )
assume a in rng h ; :: thesis: 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 g ; :: thesis: not a nin F2()
hence not a nin F2() by ZFMISC_1:87; :: thesis: verum
end;
suppose [x,a] in {[(EmptyIns F1()),F3()]} ; :: thesis: not a nin F2()
then [x,a] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then a = F3() by XTUPLE_0:1;
hence not a nin F2() ; :: thesis: verum
end;
suppose [x,a] in H1(i,g) ; :: thesis: 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() ; :: thesis: verum
end;
suppose [x,a] in H2(i,g) ; :: thesis: 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() ; :: thesis: verum
end;
suppose [x,a] in H3(i,g) ; :: thesis: 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() ; :: thesis: 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 ; :: thesis: ( 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) ; :: thesis: ( ( 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 :: thesis: ( ( 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) ; :: thesis: 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; :: thesis: verum
end;
hereby :: thesis: ( ( 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(); :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum
end;
hereby :: thesis: 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(); :: thesis: ( 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) ; :: thesis: 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; :: thesis: verum
end;
let C, I be Element of F1(); :: thesis: ( 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) ; :: thesis: 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; :: thesis: 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
hereby :: according to RELAT_1:def 1 :: thesis: Union FF is Function-like
let x be object ; :: thesis: ( x in Union FF implies ex a, b being object st x = [a,b] )
assume x in Union FF ; :: thesis: ex a, b being object st x = [a,b]
then consider n being object such that
A167: n in dom FF and
A168: x in FF . n by CARD_5:2;
reconsider n = n as Element of NAT by A3, A167;
S1[n] by A166;
hence ex a, b being object st x = [a,b] by A168, RELAT_1:def 1; :: thesis: verum
end;
let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( [x,y1] nin Union FF or [x,y2] nin Union FF or y1 = y2 )
assume [x,y1] in Union FF ; :: thesis: ( [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 ; :: thesis: 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; :: thesis: verum
end;
then reconsider f = Union FF as Function ;
A173: dom f = the carrier of F1()
proof
thus dom f c= the carrier of F1() :: according to XBOOLE_0:def 10 :: thesis: the carrier of F1() c= dom f
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin dom f or not x nin the carrier of F1() )
assume x in dom f ; :: thesis: not x nin the carrier of F1()
then [x,(f . x)] in f by FUNCT_1:def 2;
then consider n being object such that
A174: n in dom FF and
A175: [x,(f . x)] in FF . n by CARD_5:2;
reconsider n = n as Element of NAT by A3, A174;
S1[n] by A166;
then x in (ElementaryInstructions F1()) |^ n by A175, ZFMISC_1:87;
hence not x nin the carrier of F1() ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin the carrier of F1() or not x nin dom f )
assume x in the carrier of F1() ; :: thesis: not x nin dom f
then reconsider I = x as Element of F1() ;
consider n being Nat such that
A176: I in (ElementaryInstructions F1()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n] by A166;
then reconsider g = FF . n as Function of ((ElementaryInstructions F1()) |^ n),F2() ;
dom g = (ElementaryInstructions F1()) |^ n by FUNCT_2:def 1;
then [I,(g . I)] in g by A176, FUNCT_1:def 2;
then [I,(g . I)] in f by A3, CARD_5:2;
hence not x nin dom f by XTUPLE_0:def 12; :: thesis: verum
end;
rng f c= F2()
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( b nin rng f or not b nin F2() )
assume b in rng f ; :: thesis: not b nin F2()
then consider a being object such that
A177: a in dom f and
A178: b = f . a by FUNCT_1:def 3;
reconsider a = a as Element of F1() by A173, A177;
consider n being Nat such that
A179: a in (ElementaryInstructions F1()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S1[n] by A166;
then reconsider g = FF . n as Function of ((ElementaryInstructions F1()) |^ n),F2() ;
A180: dom g = (ElementaryInstructions F1()) |^ n by FUNCT_2:def 1;
then [a,(g . a)] in g by A179, FUNCT_1:def 2;
then [a,(g . a)] in f by A3, CARD_5:2;
then A181: b = g . a by A178, FUNCT_1:1;
g . a in rng g by A179, A180, FUNCT_1:3;
hence not b nin F2() by A181; :: thesis: verum
end;
then reconsider f = f as Function of the carrier of F1(),F2() by A173, FUNCT_2:2;
take f ; :: thesis: ( ( 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 :: thesis: ( 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)) ) )
let I be Element of F1(); :: thesis: ( I in ElementaryInstructions F1() implies f . I = F4(I) )
assume I in ElementaryInstructions F1() ; :: thesis: f . I = F4(I)
then [I,F4(I)] in FF . 0 by A3;
then [I,F4(I)] in f by A3, CARD_5:2;
hence f . I = F4(I) by FUNCT_1:1; :: thesis: verum
end;
A182: now :: thesis: for n being Nat
for I being Element of F1()
for g being Function of ((ElementaryInstructions F1()) |^ n),F2() st I in (ElementaryInstructions F1()) |^ n & g = FF . n holds
g . I = f . I
let n be Nat; :: thesis: for I being Element of F1()
for g being Function of ((ElementaryInstructions F1()) |^ n),F2() st I in (ElementaryInstructions F1()) |^ n & g = FF . n holds
g . I = f . I
let I be Element of F1(); :: thesis: for g being Function of ((ElementaryInstructions F1()) |^ n),F2() st I in (ElementaryInstructions F1()) |^ n & g = FF . n holds
g . I = f . I
let g be Function of ((ElementaryInstructions F1()) |^ n),F2(); :: thesis: ( I in (ElementaryInstructions F1()) |^ n & g = FF . n implies g . I = f . I )
assume that
A183: I in (ElementaryInstructions F1()) |^ n and
A184: g = FF . n ; :: thesis: g . I = f . I
dom g = (ElementaryInstructions F1()) |^ n by FUNCT_2:def 1;
then A185: [I,(g . I)] in g by A183, FUNCT_1:def 2;
n in NAT by ORDINAL1:def 12;
then [I,(g . I)] in f by A3, A184, A185, CARD_5:2;
hence g . I = f . I by FUNCT_1:1; :: thesis: verum
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; :: thesis: ( ( 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 :: thesis: ( ( 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(); :: thesis: 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; :: thesis: verum
end;
hereby :: thesis: 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(); :: thesis: 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; :: thesis: verum
end;
let C, I be Element of F1(); :: thesis: 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; :: thesis: verum