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 13;
A7: m = n + i by A6;
defpred S1[ Nat] means FF . n c= FF . (n + $1);
A8: S1[ 0 ] ;
A9: now
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
FF . ((n' + i) + 1) = H4(n' + i,FF . (n' + 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 Element of NAT holds S1[i] from NAT_1:sch 1(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 set ; :: 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 4;
then ex I being Element of F1() st
( [x,(f0 . x)] = [I,F4(I)] & S2[I] ) ;
hence not x nin ElementaryInstructions F1() by ZFMISC_1:33; :: thesis: verum
end;
let x be set ; :: 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 RELAT_1:def 4; :: thesis: verum
end;
rng f0 c= F2()
proof
let y be set ; :: 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 set such that
A12: [x,y] in f0 by RELAT_1:def 5;
consider I being Element of F1() such that
A13: ( [x,y] = [I,F4(I)] & S2[I] ) by A12;
y = F4(I) by A13, ZFMISC_1:33;
hence not y nin F2() by A1, A13; :: thesis: verum
end;
then reconsider f0 = f0 as Function of ((ElementaryInstructions F1()) |^ 0 ),F2() by A2, A10, FUNCT_2:4;
A14: 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
let I1, I2 be Element of F1(); :: thesis: I1 \; I2 nin ElementaryInstructions F1()
( I1 \; I2 <> I1 & I1 \; I2 <> I2 ) by Th73;
hence I1 \; I2 nin ElementaryInstructions F1() by 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;
A15: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
given g being Function of ((ElementaryInstructions F1()) |^ i),F2() such that A16: ( g = FF . i & ( EmptyIns F1() in (ElementaryInstructions F1()) |^ i implies g . (EmptyIns F1()) = F3() ) & ( for I1, I2 being Element of F1() st I1 \; I2 in (ElementaryInstructions F1()) |^ i 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()) |^ i 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()) |^ i holds
g . (while C,I) = F6((g . C),(g . I)) ) ) ; :: thesis: S1[i + 1]
set h = FF . (i + 1);
i < i + 1 by NAT_1:13;
then A17: ( FF . (i + 1) = H4(i,g) & dom g = (ElementaryInstructions F1()) |^ i & (ElementaryInstructions F1()) |^ i c= (ElementaryInstructions F1()) |^ (i + 1) ) by A4, A16, Th21, FUNCT_2:def 1;
A18: now
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 A17, 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 set ; :: according to RELAT_1:def 1 :: thesis: ( x nin FF . (i + 1) or ex b1, b2 being set st x = [b1,b2] )
assume x in FF . (i + 1) ; :: thesis: ex b1, b2 being set 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 A18;
then ( ex a, b being set 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 set 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 set ; :: 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 A19: [x,y1] in h ; :: thesis: ( [x,y2] nin h or y1 = y2 )
assume A20: [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 A18, A19;
suppose A21: [x,y1] in g ; :: thesis: y1 = y2
then A22: ( x in dom g & y1 = g . x ) by FUNCT_1:8;
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 A18, A20;
suppose [x,y2] in g ; :: thesis: y1 = y2
hence y1 = y2 by A21, FUNCT_1:def 1; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then ( x = EmptyIns F1() & y2 = F3() ) by ZFMISC_1:33;
hence y1 = y2 by A16, A22; :: 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
A23: ( [x,y2] = [(J1 \; J2),F5(gJ1,gJ2)] & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [J1,gJ1] in g & [J2,gJ2] in g ) ;
( x = J1 \; J2 & y2 = F5(gJ1,gJ2) & g . J1 = gJ1 & g . J2 = gJ2 ) by A23, FUNCT_1:8, ZFMISC_1:33;
hence y1 = y2 by A16, A22; :: 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
A24: ( [x,y2] = [(if-then-else D,J1,J2),F7(a,b,c)] & D in (ElementaryInstructions F1()) |^ i & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J1,b] in g & [J2,c] in g ) ;
( x = if-then-else D,J1,J2 & y2 = F7(a,b,c) & g . D = a & g . J1 = b & g . J2 = c ) by A24, FUNCT_1:8, ZFMISC_1:33;
hence y1 = y2 by A16, A22; :: 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
A25: ( [x,y2] = [(while D,J),F6(a,b)] & D in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J,b] in g ) ;
( x = while D,J & y2 = F6(a,b) & g . D = a & g . J = b ) by A25, FUNCT_1:8, ZFMISC_1:33;
hence y1 = y2 by A16, A22; :: thesis: verum
end;
end;
end;
suppose [x,y1] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then A26: [x,y1] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then A27: ( x = EmptyIns F1() & y1 = F3() ) by ZFMISC_1:33;
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 A18, A20;
suppose [x,y2] in g ; :: thesis: y1 = y2
then ( x in dom g & y2 = g . x ) by FUNCT_1:8;
hence y1 = y2 by A27, A16; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
hence y1 = y2 by A26, ZFMISC_1:33; :: 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
A28: ( [x,y2] = [(J1 \; J2),F5(a,b)] & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [J1,a] in g & [J2,b] in g ) ;
x = J1 \; J2 by A28, ZFMISC_1:33;
hence y1 = y2 by A27, 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
A29: ( [x,y2] = [(if-then-else D,J1,J2),F7(a,b,c)] & D in (ElementaryInstructions F1()) |^ i & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J1,b] in g & [J2,c] in g ) ;
x = if-then-else D,J1,J2 by A29, ZFMISC_1:33;
hence y1 = y2 by A27, 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
A30: ( [x,y2] = [(while D,J),F6(a,b)] & D in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J,b] in g ) ;
x = while D,J by A30, ZFMISC_1:33;
hence y1 = y2 by A27, 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
A31: ( [x,y1] = [(I1 \; I2),F5(gI1,gI2)] & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i & [I1,gI1] in g & [I2,gI2] in g ) ;
A32: ( x = I1 \; I2 & y1 = F5(gI1,gI2) & g . I1 = gI1 & g . I2 = gI2 ) by A31, FUNCT_1:8, ZFMISC_1:33;
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 A18, A20;
suppose [x,y2] in g ; :: thesis: y1 = y2
then ( x in dom g & y2 = g . x ) by FUNCT_1:8;
hence y1 = y2 by A32, A16; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then ( x = EmptyIns F1() & y2 = F3() ) by ZFMISC_1:33;
hence y1 = y2 by A32, 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
A33: ( [x,y2] = [(J1 \; J2),F5(a,b)] & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [J1,a] in g & [J2,b] in g ) ;
A34: ( x = J1 \; J2 & y2 = F5(a,b) & g . J1 = a & g . J2 = b ) by A33, FUNCT_1:8, ZFMISC_1:33;
then ( I1 = J1 & I2 = J2 ) by A32, Th73;
hence y1 = y2 by A32, A34; :: 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
A35: ( [x,y2] = [(if-then-else D,J1,J2),F7(a,b,c)] & D in (ElementaryInstructions F1()) |^ i & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J1,b] in g & [J2,c] in g ) ;
x = if-then-else D,J1,J2 by A35, ZFMISC_1:33;
hence y1 = y2 by A32, 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
A36: ( [x,y2] = [(while D,J),F6(a,b)] & D in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J,b] in g ) ;
x = while D,J by A36, ZFMISC_1:33;
hence y1 = y2 by A32, 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
A37: ( [x,y1] = [(if-then-else C,I1,I2),F7(gC,gI1,gI2)] & C in (ElementaryInstructions F1()) |^ i & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i & [C,gC] in g & [I1,gI1] in g & [I2,gI2] in g ) ;
A38: ( x = if-then-else C,I1,I2 & y1 = F7(gC,gI1,gI2) & g . I1 = gI1 & g . I2 = gI2 & g . C = gC ) by A37, FUNCT_1:8, ZFMISC_1:33;
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 A18, A20;
suppose [x,y2] in g ; :: thesis: y1 = y2
then ( x in dom g & y2 = g . x ) by FUNCT_1:8;
hence y1 = y2 by A38, A16; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then ( x = EmptyIns F1() & y2 = F3() ) by ZFMISC_1:33;
hence y1 = y2 by A38, 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
A39: ( [x,y2] = [(J1 \; J2),F5(a,b)] & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [J1,a] in g & [J2,b] in g ) ;
x = J1 \; J2 by A39, ZFMISC_1:33;
hence y1 = y2 by A38, 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
A40: ( [x,y2] = [(if-then-else D,J1,J2),F7(a,b,c)] & D in (ElementaryInstructions F1()) |^ i & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J1,b] in g & [J2,c] in g ) ;
A41: ( x = if-then-else D,J1,J2 & y2 = F7(a,b,c) & g . D = a & g . J1 = b & g . J2 = c ) by A40, FUNCT_1:8, ZFMISC_1:33;
then ( C = D & I1 = J1 & I2 = J2 ) by A38, Th74;
hence y1 = y2 by A38, A41; :: 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
A42: ( [x,y2] = [(while D,J),F6(a,b)] & D in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J,b] in g ) ;
x = while D,J by A42, ZFMISC_1:33;
hence y1 = y2 by A38, 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
A43: ( [x,y1] = [(while C,I),F6(gC,gI)] & C in (ElementaryInstructions F1()) |^ i & I in (ElementaryInstructions F1()) |^ i & [C,gC] in g & [I,gI] in g ) ;
A44: ( x = while C,I & y1 = F6(gC,gI) & g . C = gC & g . I = gI ) by A43, FUNCT_1:8, ZFMISC_1:33;
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 A18, A20;
suppose [x,y2] in g ; :: thesis: y1 = y2
then ( x in dom g & y2 = g . x ) by FUNCT_1:8;
hence y1 = y2 by A44, A16; :: thesis: verum
end;
suppose [x,y2] in {[(EmptyIns F1()),F3()]} ; :: thesis: y1 = y2
then [x,y2] = [(EmptyIns F1()),F3()] by TARSKI:def 1;
then ( x = EmptyIns F1() & y2 = F3() ) by ZFMISC_1:33;
hence y1 = y2 by A44, 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
A45: ( [x,y2] = [(J1 \; J2),F5(a,b)] & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [J1,a] in g & [J2,b] in g ) ;
x = J1 \; J2 by A45, ZFMISC_1:33;
hence y1 = y2 by A44, 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
A46: ( [x,y2] = [(if-then-else D,J1,J2),F7(a,b,c)] & D in (ElementaryInstructions F1()) |^ i & J1 in (ElementaryInstructions F1()) |^ i & J2 in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J1,b] in g & [J2,c] in g ) ;
x = if-then-else D,J1,J2 by A46, ZFMISC_1:33;
hence y1 = y2 by A44, 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
A47: ( [x,y2] = [(while D,J),F6(a,b)] & D in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [D,a] in g & [J,b] in g ) ;
A48: ( x = while D,J & y2 = F6(a,b) & g . D = a & g . J = b ) by A47, FUNCT_1:8, ZFMISC_1:33;
then ( D = C & J = I ) by A44, Th75;
hence y1 = y2 by A44, A48; :: thesis: verum
end;
end;
end;
end;
end;
then reconsider h = h as Function ;
A49: 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 set ; :: 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 A50: [a,(h . a)] in h by FUNCT_1:def 4;
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 A18, A50;
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 ZFMISC_1:33;
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
A51: ( [a,(h . a)] = [(I \; J),F5(e,b)] & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [I,e] in g & [J,b] in g ) ;
a = I \; J by A51, ZFMISC_1:33;
hence not a nin (ElementaryInstructions F1()) |^ (i + 1) by A51, 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
A52: ( [a,(h . a)] = [(if-then-else C,I,J),F7(e,b,c)] & C in (ElementaryInstructions F1()) |^ i & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [C,e] in g & [I,b] in g & [J,c] in g ) ;
a = if-then-else C,I,J by A52, ZFMISC_1:33;
hence not a nin (ElementaryInstructions F1()) |^ (i + 1) by A52, 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
A53: ( [a,(h . a)] = [(while I,J),F6(e,b)] & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [I,e] in g & [J,b] in g ) ;
a = while I,J by A53, ZFMISC_1:33;
hence not a nin (ElementaryInstructions F1()) |^ (i + 1) by A53, Th76; :: thesis: verum
end;
end;
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin (ElementaryInstructions F1()) |^ (i + 1) or not x nin dom h )
assume A54: 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 A54, Th77;
suppose x in (ElementaryInstructions F1()) |^ i ; :: thesis: not x nin dom h
then [x,(g . x)] in g by A17, FUNCT_1:def 4;
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 A17, XBOOLE_0:def 3;
hence not x nin dom h by RELAT_1:def 4; :: 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 A17, XBOOLE_0:def 3;
hence not x nin dom h by RELAT_1:def 4; :: 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
A55: ( x = I1 \; I2 & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i ) ;
reconsider a = g . I1, b = g . I2 as Element of F2() by A55, FUNCT_2:7;
( [I1,a] in g & [I2,b] in g ) by A17, A55, FUNCT_1:def 4;
then [x,F5(a,b)] in H1(i,g) by A55;
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 A17, XBOOLE_0:def 3;
hence not x nin dom h by RELAT_1:def 4; :: 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
A56: ( x = if-then-else C,I1,I2 & C in (ElementaryInstructions F1()) |^ i & I1 in (ElementaryInstructions F1()) |^ i & I2 in (ElementaryInstructions F1()) |^ i ) ;
reconsider a = g . I1, b = g . I2, c = g . C as Element of F2() by A56, FUNCT_2:7;
( [I1,a] in g & [I2,b] in g & [C,c] in g ) by A17, A56, FUNCT_1:def 4;
then [x,F7(c,a,b)] in H2(i,g) by A56;
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 A17, XBOOLE_0:def 3;
hence not x nin dom h by RELAT_1:def 4; :: 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
A57: ( x = while C,I & C in (ElementaryInstructions F1()) |^ i & I in (ElementaryInstructions F1()) |^ i ) ;
reconsider a = g . C, b = g . I as Element of F2() by A57, FUNCT_2:7;
( [C,a] in g & [I,b] in g ) by A17, A57, FUNCT_1:def 4;
then [x,F6(a,b)] in H3(i,g) by A57;
then [x,F6(a,b)] in h by A17, XBOOLE_0:def 3;
hence not x nin dom h by RELAT_1:def 4; :: thesis: verum
end;
end;
end;
rng h c= F2()
proof
let a be set ; :: 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 set such that
A58: [x,a] in h by RELAT_1:def 5;
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 A18, A58;
suppose [x,a] in g ; :: thesis: not a nin F2()
hence not a nin F2() by ZFMISC_1:106; :: 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 ZFMISC_1:33;
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
A59: ( [x,a] = [(I \; J),F5(e,b)] & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [I,e] in g & [J,b] in g ) ;
a = F5(e,b) by A59, ZFMISC_1:33;
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
A60: ( [x,a] = [(if-then-else C,I,J),F7(e,b,c)] & C in (ElementaryInstructions F1()) |^ i & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [C,e] in g & [I,b] in g & [J,c] in g ) ;
a = F7(e,b,c) by A60, ZFMISC_1:33;
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
A61: ( [x,a] = [(while I,J),F6(e,b)] & I in (ElementaryInstructions F1()) |^ i & J in (ElementaryInstructions F1()) |^ i & [I,e] in g & [J,b] in g ) ;
a = F6(e,b) by A61, ZFMISC_1:33;
hence not a nin F2() ; :: thesis: verum
end;
end;
end;
then reconsider h = h as Function of ((ElementaryInstructions F1()) |^ (i + 1)),F2() by A49, FUNCT_2:4;
h = ((g \/ {[(EmptyIns F1()),F3()]}) \/ H1(i,g)) \/ (H2(i,g) \/ H3(i,g)) by A17, 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 A62: 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 A17, XBOOLE_0:def 3;
hence h . (EmptyIns F1()) = F3() by FUNCT_1:8; :: 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 consider i0 being Nat such that
A63: ( i + 1 = i0 + 1 & I1 in (ElementaryInstructions F1()) |^ i0 & I2 in (ElementaryInstructions F1()) |^ i0 ) by Th88;
reconsider gI1 = g . I1, gI2 = g . I2 as Element of F2() by A63, FUNCT_2:7;
A64: ( [I1,gI1] in g & [I2,gI2] in g ) by A17, A63, FUNCT_1:def 4;
then ( g . I1 = h . I1 & g . I2 = h . I2 ) by A62, FUNCT_1:8;
then [(I1 \; I2),F5((h . I1),(h . I2))] in H1(i,g) by A63, A64;
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 A17, XBOOLE_0:def 3;
hence h . (I1 \; I2) = F5((h . I1),(h . I2)) by FUNCT_1:8; :: 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 consider i0 being Nat such that
A65: ( i + 1 = i0 + 1 & C in (ElementaryInstructions F1()) |^ i0 & I1 in (ElementaryInstructions F1()) |^ i0 & I2 in (ElementaryInstructions F1()) |^ i0 ) by Th89;
reconsider gC = g . C, gI1 = g . I1, gI2 = g . I2 as Element of F2() by A65, FUNCT_2:7;
A66: ( [C,gC] in g & [I1,gI1] in g & [I2,gI2] in g ) by A17, A65, FUNCT_1:def 4;
then ( g . C = h . C & g . I1 = h . I1 & g . I2 = h . I2 ) by A62, FUNCT_1:8;
then [(if-then-else C,I1,I2),F7((h . C),(h . I1),(h . I2))] in H2(i,g) by A65, A66;
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 A17, XBOOLE_0:def 3;
hence h . (if-then-else C,I1,I2) = F7((h . C),(h . I1),(h . I2)) by FUNCT_1:8; :: 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 consider i0 being Nat such that
A67: ( i + 1 = i0 + 1 & C in (ElementaryInstructions F1()) |^ i0 & I in (ElementaryInstructions F1()) |^ i0 ) by Th90;
reconsider gC = g . C, gI = g . I as Element of F2() by A67, FUNCT_2:7;
A68: ( [C,gC] in g & [I,gI] in g ) by A17, A67, FUNCT_1:def 4;
then ( g . C = h . C & g . I = h . I ) by A62, FUNCT_1:8;
then [(while C,I),F6((h . C),(h . I))] in H3(i,g) by A67, A68;
then [(while C,I),F6((h . C),(h . I))] in h by A17, XBOOLE_0:def 3;
hence h . (while C,I) = F6((h . C),(h . I)) by FUNCT_1:8; :: thesis: verum
end;
A69: for i being Element of NAT holds S1[i] from NAT_1:sch 1(A14, A15);
 ( 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 set ; :: thesis: ( x in Union FF implies ex a, b being set st x = [a,b] )
assume x in Union FF ; :: thesis: ex a, b being set st x = [a,b]
then consider n being set such that
A70: ( n in dom FF & x in FF . n ) by CARD_5:10;
reconsider n = n as Element of NAT by A3, A70;
S1[n] by A69;
hence ex a, b being set st x = [a,b] by A70, RELAT_1:def 1; :: thesis: verum
end;
let x, y1, y2 be set ; :: 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 set such that
A71: ( n1 in dom FF & [x,y1] in FF . n1 ) by CARD_5:10;
assume [x,y2] in Union FF ; :: thesis: y1 = y2
then consider n2 being set such that
A72: ( n2 in dom FF & [x,y2] in FF . n2 ) by CARD_5:10;
reconsider n1 = n1, n2 = n2 as Element of NAT by A3, A71, A72;
( 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 A71, A72, A69;
hence y1 = y2 by A71, A72, FUNCT_1:def 1; :: thesis: verum
end;
then reconsider f = Union FF as Function ;
A73: 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 set ; :: 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 4;
then consider n being set such that
A74: ( n in dom FF & [x,(f . x)] in FF . n ) by CARD_5:10;
reconsider n = n as Element of NAT by A3, A74;
S1[n] by A69;
then x in (ElementaryInstructions F1()) |^ n by A74, ZFMISC_1:106;
hence not x nin the carrier of F1() ; :: thesis: verum
end;
let x be set ; :: 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
A75: I in (ElementaryInstructions F1()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
S1[n] by A69;
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 A75, FUNCT_1:def 4;
then [I,(g . I)] in f by A3, CARD_5:10;
hence not x nin dom f by RELAT_1:def 4; :: thesis: verum
end;
rng f c= F2()
proof
let b be set ; :: 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 set such that
A76: ( a in dom f & b = f . a ) by FUNCT_1:def 5;
reconsider a = a as Element of F1() by A73, A76;
consider n being Nat such that
A77: a in (ElementaryInstructions F1()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
S1[n] by A69;
then reconsider g = FF . n as Function of ((ElementaryInstructions F1()) |^ n),F2() ;
A78: dom g = (ElementaryInstructions F1()) |^ n by FUNCT_2:def 1;
then [a,(g . a)] in g by A77, FUNCT_1:def 4;
then [a,(g . a)] in f by A3, CARD_5:10;
then ( b = g . a & g . a in rng g & rng g c= F2() ) by A76, A77, A78, FUNCT_1:8, FUNCT_1:12;
hence not b nin F2() ; :: thesis: verum
end;
then reconsider f = f as Function of the carrier of F1(),F2() by A73, FUNCT_2:4;
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:10;
hence f . I = F4(I) by FUNCT_1:8; :: thesis: verum
end;
A79: now
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 A80: ( I in (ElementaryInstructions F1()) |^ n & g = FF . n ) ; :: thesis: g . I = f . I
dom g = (ElementaryInstructions F1()) |^ n by FUNCT_2:def 1;
then ( [I,(g . I)] in g & n in NAT ) by A80, FUNCT_1:def 4, ORDINAL1:def 13;
then [I,(g . I)] in f by A3, A80, CARD_5:10;
hence g . I = f . I by FUNCT_1:8; :: thesis: verum
end;
consider n0 being Nat such that
A81: EmptyIns F1() in (ElementaryInstructions F1()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 13;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A82: ( g0 = FF . n0 & ( 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)) ) & ( 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)) ) & ( 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 A69;
dom g0 = (ElementaryInstructions F1()) |^ n0 by FUNCT_2:def 1;
then [(EmptyIns F1()),F3()] in g0 by A81, A82, FUNCT_1:def 4;
then [(EmptyIns F1()),F3()] in f by A3, A82, CARD_5:10;
hence f . (EmptyIns F1()) = F3() by FUNCT_1:8; :: 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
A83: I1 \; I2 in (ElementaryInstructions F1()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 13;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A84: g0 = FF . n0 and
( EmptyIns F1() in (ElementaryInstructions F1()) |^ n0 implies g0 . (EmptyIns F1()) = F3() ) and
A85: 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)) ) & ( 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 A69;
consider i0 being Nat such that
A86: ( n0 = i0 + 1 & I1 in (ElementaryInstructions F1()) |^ i0 & I2 in (ElementaryInstructions F1()) |^ i0 ) by A83, Th88;
n0 > i0 by A86, NAT_1:13;
then (ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0 by Th21;
then ( dom g0 = (ElementaryInstructions F1()) |^ n0 & g0 . I1 = f . I1 & g0 . I2 = f . I2 ) by A79, A84, A86, FUNCT_2:def 1;
then ( [(I1 \; I2),(g0 . (I1 \; I2))] in g0 & g0 . (I1 \; I2) = F5((f . I1),(f . I2)) ) by A83, A85, FUNCT_1:8;
then [(I1 \; I2),F5((f . I1),(f . I2))] in f by A3, A84, CARD_5:10;
hence f . (I1 \; I2) = F5((f . I1),(f . I2)) by FUNCT_1:8; :: 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
A87: if-then-else C,I1,I2 in (ElementaryInstructions F1()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 13;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A88: 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
A89: 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 A69;
consider i0 being Nat such that
A90: ( n0 = i0 + 1 & C in (ElementaryInstructions F1()) |^ i0 & I1 in (ElementaryInstructions F1()) |^ i0 & I2 in (ElementaryInstructions F1()) |^ i0 ) by A87, Th89;
n0 > i0 by A90, NAT_1:13;
then (ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0 by Th21;
then ( dom g0 = (ElementaryInstructions F1()) |^ n0 & g0 . C = f . C & g0 . I1 = f . I1 & g0 . I2 = f . I2 ) by A79, A88, A90, FUNCT_2:def 1;
then ( [(if-then-else C,I1,I2),(g0 . (if-then-else C,I1,I2))] in g0 & g0 . (if-then-else C,I1,I2) = F7((f . C),(f . I1),(f . I2)) ) by A87, A89, FUNCT_1:8;
then [(if-then-else C,I1,I2),F7((f . C),(f . I1),(f . I2))] in f by A3, A88, CARD_5:10;
hence f . (if-then-else C,I1,I2) = F7((f . C),(f . I1),(f . I2)) by FUNCT_1:8; :: 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
A91: while C,I in (ElementaryInstructions F1()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 13;
consider g0 being Function of ((ElementaryInstructions F1()) |^ n0),F2() such that
A92: 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
A93: 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 A69;
consider i0 being Nat such that
A94: ( n0 = i0 + 1 & C in (ElementaryInstructions F1()) |^ i0 & I in (ElementaryInstructions F1()) |^ i0 ) by A91, Th90;
n0 > i0 by A94, NAT_1:13;
then (ElementaryInstructions F1()) |^ i0 c= (ElementaryInstructions F1()) |^ n0 by Th21;
then ( dom g0 = (ElementaryInstructions F1()) |^ n0 & g0 . C = f . C & g0 . I = f . I ) by A79, A92, A94, FUNCT_2:def 1;
then ( [(while C,I),(g0 . (while C,I))] in g0 & g0 . (while C,I) = F6((f . C),(f . I)) ) by A91, A93, FUNCT_1:8;
then [(while C,I),F6((f . C),(f . I))] in f by A3, A92, CARD_5:10;
hence f . (while C,I) = F6((f . C),(f . I)) by FUNCT_1:8; :: thesis: verum