set QQ = { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ;
set IT = meet { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ;
S1[ [#] [:S, the carrier of A:]]
proof
set Y = [#] [:S, the carrier of A:];
{(EmptyIns A)} c= the carrier of A by ZFMISC_1:31;
hence ( [:S,(ElementaryInstructions A):] c= [#] [:S, the carrier of A:] & [:S,{(EmptyIns A)}:] c= [#] [:S, the carrier of A:] ) by ZFMISC_1:95; :: thesis: for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in [#] [:S, the carrier of A:] & [(f . (s,I)),J] in [#] [:S, the carrier of A:] implies [s,(I \; J)] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & [(f . (s,C)),I] in [#] [:S, the carrier of A:] & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & [(f . (s,C)),J] in [#] [:S, the carrier of A:] & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in [#] [:S, the carrier of A:] & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in [#] [:S, the carrier of A:] ) )
thus for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in [#] [:S, the carrier of A:] & [(f . (s,I)),J] in [#] [:S, the carrier of A:] implies [s,(I \; J)] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & [(f . (s,C)),I] in [#] [:S, the carrier of A:] & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & [(f . (s,C)),J] in [#] [:S, the carrier of A:] & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in [#] [:S, the carrier of A:] ) & ( [s,C] in [#] [:S, the carrier of A:] & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in [#] [:S, the carrier of A:] & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in [#] [:S, the carrier of A:] ) ) by ZFMISC_1:87; :: thesis: verum
end;
then A1: [:S, the carrier of A:] in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ;
then reconsider IT = meet { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } as Subset of [:S, the carrier of A:] by SETFAM_1:3;
take IT ; :: thesis: ( [:S,(ElementaryInstructions A):] c= IT & [:S,{(EmptyIns A)}:] c= IT & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in IT & [(f . (s,I)),J] in IT implies [s,(I \; J)] in IT ) & ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
IT c= P ) )
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[:S,(ElementaryInstructions A):] c= a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [:S,(ElementaryInstructions A):] c= a )
assume a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [:S,(ElementaryInstructions A):] c= a
then ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) ;
hence [:S,(ElementaryInstructions A):] c= a ; :: thesis: verum
end;
hence [:S,(ElementaryInstructions A):] c= IT by A1, SETFAM_1:5; :: thesis: ( [:S,{(EmptyIns A)}:] c= IT & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in IT & [(f . (s,I)),J] in IT implies [s,(I \; J)] in IT ) & ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
IT c= P ) )
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[:S,{(EmptyIns A)}:] c= a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [:S,{(EmptyIns A)}:] c= a )
assume a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [:S,{(EmptyIns A)}:] c= a
then ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) ;
hence [:S,{(EmptyIns A)}:] c= a ; :: thesis: verum
end;
hence [:S,{(EmptyIns A)}:] c= IT by A1, SETFAM_1:5; :: thesis: ( ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in IT & [(f . (s,I)),J] in IT implies [s,(I \; J)] in IT ) & ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) ) ) & ( for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
IT c= P ) )
hereby :: thesis: for P being Subset of [:S, the carrier of A:] st [:S,(ElementaryInstructions A):] c= P & [:S,{(EmptyIns A)}:] c= P & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in P & [(f . (s,I)),J] in P implies [s,(I \; J)] in P ) & ( [s,C] in P & [(f . (s,C)),I] in P & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & [(f . (s,C)),J] in P & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in P ) & ( [s,C] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in P ) ) ) holds
IT c= P
let s be Element of S; :: thesis: for C, I, J being Element of A holds
( ( [s,I] in IT & [(f . (s,I)),J] in IT implies [s,(I \; J)] in IT ) & ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) )
let C, I, J be Element of A; :: thesis: ( ( [s,I] in IT & [(f . (s,I)),J] in IT implies [s,(I \; J)] in IT ) & ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) )
hereby :: thesis: ( ( [s,C] in IT & [(f . (s,C)),I] in IT & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) )
assume that
A2: [s,I] in IT and
A3: [(f . (s,I)),J] in IT ; :: thesis: [s,(I \; J)] in IT
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[s,(I \; J)] in a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [s,(I \; J)] in a )
assume A4: a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [s,(I \; J)] in a
then A5: [s,I] in a by A2, SETFAM_1:def 1;
A6: [(f . (s,I)),J] in a by A3, A4, SETFAM_1:def 1;
ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) by A4;
hence [s,(I \; J)] in a by A5, A6; :: thesis: verum
end;
hence [s,(I \; J)] in IT by A1, SETFAM_1:def 1; :: thesis: verum
end;
hereby :: thesis: ( ( [s,C] in IT & [(f . (s,C)),J] in IT & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in IT ) & ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT ) )
assume that
A7: [s,C] in IT and
A8: [(f . (s,C)),I] in IT and
A9: f . (s,C) in T ; :: thesis: [s,(if-then-else (C,I,J))] in IT
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[s,(if-then-else (C,I,J))] in a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [s,(if-then-else (C,I,J))] in a )
assume A10: a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [s,(if-then-else (C,I,J))] in a
then A11: [s,C] in a by A7, SETFAM_1:def 1;
A12: [(f . (s,C)),I] in a by A8, A10, SETFAM_1:def 1;
ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) by A10;
hence [s,(if-then-else (C,I,J))] in a by A9, A11, A12; :: thesis: verum
end;
hence [s,(if-then-else (C,I,J))] in IT by A1, SETFAM_1:def 1; :: thesis: verum
end;
hereby :: thesis: ( [s,C] in IT & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT )
assume that
A13: [s,C] in IT and
A14: [(f . (s,C)),J] in IT and
A15: f . (s,C) nin T ; :: thesis: [s,(if-then-else (C,I,J))] in IT
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[s,(if-then-else (C,I,J))] in a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [s,(if-then-else (C,I,J))] in a )
assume A16: a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [s,(if-then-else (C,I,J))] in a
then A17: [s,C] in a by A13, SETFAM_1:def 1;
A18: [(f . (s,C)),J] in a by A14, A16, SETFAM_1:def 1;
ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) by A16;
hence [s,(if-then-else (C,I,J))] in a by A15, A17, A18; :: thesis: verum
end;
hence [s,(if-then-else (C,I,J))] in IT by A1, SETFAM_1:def 1; :: thesis: verum
end;
assume A19: [s,C] in IT ; :: thesis: ( ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in IT )
given r being non empty FinSequence of S such that A20: r . 1 = f . (s,C) and
A21: r . (len r) nin T and
A22: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in IT & r . (i + 1) = f . ((r . i),(I \; C)) ) ; :: thesis: [s,(while (C,I))] in IT
now :: thesis: for a being set st a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } holds
[s,(while (C,I))] in a
let a be set ; :: thesis: ( a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } implies [s,(while (C,I))] in a )
assume A23: a in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ; :: thesis: [s,(while (C,I))] in a
A24: now :: thesis: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in a & r . (i + 1) = f . ((r . i),(I \; C)) )
let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & [(r . i),(I \; C)] in a & r . (i + 1) = f . ((r . i),(I \; C)) ) )
assume that
A25: 1 <= i and
A26: i < len r ; :: thesis: ( r . i in T & [(r . i),(I \; C)] in a & r . (i + 1) = f . ((r . i),(I \; C)) )
[(r . i),(I \; C)] in IT by A22, A25, A26;
hence ( r . i in T & [(r . i),(I \; C)] in a & r . (i + 1) = f . ((r . i),(I \; C)) ) by A22, A23, A25, A26, SETFAM_1:def 1; :: thesis: verum
end;
A27: [s,C] in a by A19, A23, SETFAM_1:def 1;
ex Z being Subset of [:S, the carrier of A:] st
( a = Z & S1[Z] ) by A23;
hence [s,(while (C,I))] in a by A20, A21, A24, A27; :: thesis: verum
end;
hence [s,(while (C,I))] in IT by A1, SETFAM_1:def 1; :: thesis: verum
end;
let Y be Subset of [:S, the carrier of A:]; :: thesis: ( [:S,(ElementaryInstructions A):] c= Y & [:S,{(EmptyIns A)}:] c= Y & ( for s being Element of S
for C, I, J being Element of A holds
( ( [s,I] in Y & [(f . (s,I)),J] in Y implies [s,(I \; J)] in Y ) & ( [s,C] in Y & [(f . (s,C)),I] in Y & f . (s,C) in T implies [s,(if-then-else (C,I,J))] in Y ) & ( [s,C] in Y & [(f . (s,C)),J] in Y & f . (s,C) nin T implies [s,(if-then-else (C,I,J))] in Y ) & ( [s,C] in Y & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I \; C)] in Y & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) implies [s,(while (C,I))] in Y ) ) ) implies IT c= Y )
assume S1[Y] ; :: thesis: IT c= Y
then Y in { Z where Z is Subset of [:S, the carrier of A:] : S1[Z] } ;
hence IT c= Y by SETFAM_1:3; :: thesis: verum