let A be preIfWhileAlgebra; :: thesis: for C, I being Element of A
for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
let C, I be Element of A; :: thesis: for S being non empty set
for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
let S be non empty set ; :: thesis: for T being Subset of S
for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
let T be Subset of S; :: thesis: for s being Element of S
for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
let s be Element of S; :: thesis: for f being ExecutionFunction of A,S,T st A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) holds
( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
let f be ExecutionFunction of A,S,T; :: thesis: ( A is free & [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) implies ( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) ) )
set TP = TerminatingPrograms (A,S,T,f);
set rr = s;
set IJ = while (C,I);
assume that
A1: A is free and
A2: [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) ; :: thesis: ( [s,C] in TerminatingPrograms (A,S,T,f) & 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) )
reconsider P = (TerminatingPrograms (A,S,T,f)) \ {[s,(while (C,I))]} as Subset of [:S, the carrier of A:] ;
A3: [:S,(ElementaryInstructions A):] c= P

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( [x,y] nin [:S,(ElementaryInstructions A):] or not [x,y] nin P )
assume A4: [x,y] in [:S,(ElementaryInstructions A):] ; :: thesis: not [x,y] nin P
then y in ElementaryInstructions A by ZFMISC_1:87;
then A5: y <> while (C,I) by Th52;
A6: [:S,(ElementaryInstructions A):] c= TerminatingPrograms (A,S,T,f) by Def35;
[x,y] <> [s,(while (C,I))] by A5, XTUPLE_0:1;
then [x,y] nin {[s,(while (C,I))]} by TARSKI:def 1;
hence not [x,y] nin P by A4, A6, XBOOLE_0:def 5; :: thesis: verum

end;

A7: [:S,{(EmptyIns A)}:] c= P

proof

let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( [x,y] nin [:S,{(EmptyIns A)}:] or not [x,y] nin P )
assume A8: [x,y] in [:S,{(EmptyIns A)}:] ; :: thesis: not [x,y] nin P
then y in {(EmptyIns A)} by ZFMISC_1:87;
then y = EmptyIns A by TARSKI:def 1;
then A9: y <> while (C,I) by A1, Th72;
A10: [:S,{(EmptyIns A)}:] c= TerminatingPrograms (A,S,T,f) by Def35;
[x,y] <> [s,(while (C,I))] by A9, XTUPLE_0:1;
then [x,y] nin {[s,(while (C,I))]} by TARSKI:def 1;
hence not [x,y] nin P by A8, A10, XBOOLE_0:def 5; :: thesis: verum

end;

A11: now :: thesis: 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 ) )

let s be Element of S; :: thesis: 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 ) )
let C, I, J be Element of A; :: thesis: ( ( [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 ) )

hereby :: thesis: ( ( [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 ) )

assume that
A12: [s,I] in P and
A13: [(f . (s,I)),J] in P ; :: thesis: [s,(I \; J)] in P
A14: [s,I] in TerminatingPrograms (A,S,T,f) by A12, ZFMISC_1:56;
A15: [(f . (s,I)),J] in TerminatingPrograms (A,S,T,f) by A13, ZFMISC_1:56;
A16: while (C,I) <> I \; J by A1, Th73;
A17: [s,(I \; J)] in TerminatingPrograms (A,S,T,f) by A14, A15, Def35;
[s,(while (C,I))] <> [s,(I \; J)] by A16, XTUPLE_0:1;
hence [s,(I \; J)] in P by A17, ZFMISC_1:56; :: thesis: verum

end;

hereby :: thesis: ( [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 )

assume that
A18: [s,C] in P and
A19: [(f . (s,C)),I] in P and
A20: f . (s,C) in T ; :: thesis: [s,(if-then-else (C,I,J))] in P
A21: [s,C] in TerminatingPrograms (A,S,T,f) by A18, ZFMISC_1:56;
A22: [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) by A19, ZFMISC_1:56;
A23: while (C,I) <> if-then-else (C,I,J) by A1, Th74;
A24: [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) by A20, A21, A22, Def35;
[s,(while (C,I))] <> [s,(if-then-else (C,I,J))] by A23, XTUPLE_0:1;
hence [s,(if-then-else (C,I,J))] in P by A24, ZFMISC_1:56; :: thesis: verum

end;

hereby :: thesis: verum

assume that
A25: [s,C] in P and
A26: [(f . (s,C)),J] in P and
A27: f . (s,C) nin T ; :: thesis: [s,(if-then-else (C,I,J))] in P
A28: [s,C] in TerminatingPrograms (A,S,T,f) by A25, ZFMISC_1:56;
A29: [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) by A26, ZFMISC_1:56;
A30: while (C,I) <> if-then-else (C,I,J) by A1, Th74;
A31: [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) by A27, A28, A29, Def35;
[s,(while (C,I))] <> [s,(if-then-else (C,I,J))] by A30, XTUPLE_0:1;
hence [s,(if-then-else (C,I,J))] in P by A31, ZFMISC_1:56; :: thesis: verum

end;

end;

hereby :: 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 TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) )

assume A32: [s,C] nin TerminatingPrograms (A,S,T,f) ; :: thesis: contradiction

now :: thesis: for s being Element of S
for C9, I9, J being Element of A st [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) holds
[s,(while (C9,I9))] in P

let s be Element of S; :: thesis: for C9, I9, J being Element of A st [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) holds
[s,(while (C9,I9))] in P
let C9, I9, J be Element of A; :: thesis: ( [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) implies [s,(while (C9,I9))] in P )
assume A33: [s,C9] in P ; :: thesis: ( ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) implies [s,(while (C9,I9))] in P )
given r being non empty FinSequence of S such that A34: r . 1 = f . (s,C9) and
A35: r . (len r) nin T and
A36: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ; :: thesis: [s,(while (C9,I9))] in P

A37: now :: thesis: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) )

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) )
assume that
A38: 1 <= i and
A39: i < len r ; :: thesis: ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) )
[(r . i),(I9 \; C9)] in P by A36, A38, A39;
hence ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) by A36, A38, A39, ZFMISC_1:56; :: thesis: verum

end;

A40: [s,C9] in TerminatingPrograms (A,S,T,f) by A33, ZFMISC_1:56;
then A41: ( while (C9,I9) <> while (C,I) or s <> s ) by A1, A32, Th75;
A42: [s,(while (C9,I9))] in TerminatingPrograms (A,S,T,f) by A34, A35, A37, A40, Def35;
[s,(while (C9,I9))] <> [s,(while (C,I))] by A41, XTUPLE_0:1;
hence [s,(while (C9,I9))] in P by A42, ZFMISC_1:56; :: thesis: verum

end;

then 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 ) ) by A11;
then TerminatingPrograms (A,S,T,f) c= P by A3, A7, Def35;
hence contradiction by A2, ZFMISC_1:56; :: thesis: verum

end;

assume A43: for r being non empty FinSequence of S holds
( not r . 1 = f . (s,C) or not r . (len r) nin T or ex i being Nat st
( 1 <= i & i < len r & not ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) ) ) ; :: thesis: contradiction

now :: thesis: for s being Element of S
for C9, I9, J being Element of A st [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) holds
[s,(while (C9,I9))] in P

let s be Element of S; :: thesis: for C9, I9, J being Element of A st [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) holds
[s,(while (C9,I9))] in P
let C9, I9, J be Element of A; :: thesis: ( [s,C9] in P & ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) implies [s,(while (C9,I9))] in P )
assume A44: [s,C9] in P ; :: thesis: ( ex r being non empty FinSequence of S st
( r . 1 = f . (s,C9) & r . (len r) nin T & ( for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ) ) implies [s,(while (C9,I9))] in P )
given r being non empty FinSequence of S such that A45: r . 1 = f . (s,C9) and
A46: r . (len r) nin T and
A47: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in P & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) ; :: thesis: [s,(while (C9,I9))] in P

A48: now :: thesis: for i being Nat st 1 <= i & i < len r holds
( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) )

let i be Nat; :: thesis: ( 1 <= i & i < len r implies ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) )
assume that
A49: 1 <= i and
A50: i < len r ; :: thesis: ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) )
[(r . i),(I9 \; C9)] in P by A47, A49, A50;
hence ( r . i in T & [(r . i),(I9 \; C9)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I9 \; C9)) ) by A47, A49, A50, ZFMISC_1:56; :: thesis: verum

end;

A51: [s,C9] in TerminatingPrograms (A,S,T,f) by A44, ZFMISC_1:56;
( I <> I9 or C <> C9 or s <> s ) by A43, A45, A46, A48;
then A52: ( while (C9,I9) <> while (C,I) or s <> s ) by A1, Th75;
A53: [s,(while (C9,I9))] in TerminatingPrograms (A,S,T,f) by A45, A46, A48, A51, Def35;
[s,(while (C9,I9))] <> [s,(while (C,I))] by A52, XTUPLE_0:1;
hence [s,(while (C9,I9))] in P by A53, ZFMISC_1:56; :: thesis: verum

end;

then 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 ) ) by A11;
then TerminatingPrograms (A,S,T,f) c= P by A3, A7, Def35;
hence contradiction by A2, ZFMISC_1:56; :: thesis: verum