let A be preIfWhileAlgebra; :: thesis:
let I, J be Element of A; :: thesis:
let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let s be Element of S; :: thesis:
let f be ExecutionFunction of A,S,T; :: thesis:
set TP = TerminatingPrograms (A,S,T,f);
assume that
A1: A is free and
A2: [s,(I \; J)] in TerminatingPrograms (A,S,T,f) ; :: thesis:
reconsider P = (TerminatingPrograms (A,S,T,f)) \ {[s,(I \; J)]} as Subset of [:S, the carrier of A:] ;
A3: [:S,(ElementaryInstructions A):] c= P

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

end;

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

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

end;

set rr = s;
set IJ = I \; J;

A13: now :: thesis:

let s be Element of S; :: thesis:
let C, I, J be Element of A; :: thesis:

hereby :: thesis:

assume that
A14: [s,C] in P and
A15: [(f . (s,C)),I] in P and
A16: f . (s,C) in T ; :: thesis:
A17: [s,C] in TerminatingPrograms (A,S,T,f) by A14, ZFMISC_1:56;
A18: [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) by A15, ZFMISC_1:56;
A19: I \; J <> if-then-else (C,I,J) by A1, Th73;
A20: [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) by A16, A17, A18, Def35;
[s,(I \; J)] <> [s,(if-then-else (C,I,J))] by A19, XTUPLE_0:1;
hence [s,(if-then-else (C,I,J))] in P by A20, ZFMISC_1:56; :: thesis:

end;

hereby :: thesis:

assume that
A21: [s,C] in P and
A22: [(f . (s,C)),J] in P and
A23: f . (s,C) nin T ; :: thesis:
A24: [s,C] in TerminatingPrograms (A,S,T,f) by A21, ZFMISC_1:56;
A25: [(f . (s,C)),J] in TerminatingPrograms (A,S,T,f) by A22, ZFMISC_1:56;
A26: I \; J <> if-then-else (C,I,J) by A1, Th73;
A27: [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) by A23, A24, A25, Def35;
[s,(I \; J)] <> [s,(if-then-else (C,I,J))] by A26, XTUPLE_0:1;
hence [s,(if-then-else (C,I,J))] in P by A27, ZFMISC_1:56; :: thesis:

end;

assume A28: [s,C] in P ; :: thesis:
given r being non empty FinSequence of S such that A29: r . 1 = f . (s,C) and
A30: r . (len r) nin T and
A31: 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)) ) ; :: thesis:

A32: now :: thesis:

let i be Nat; :: thesis:
assume that
A33: 1 <= i and
A34: i < len r ; :: thesis:
[(r . i),(I \; C)] in P by A31, A33, A34;
hence ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f) & r . (i + 1) = f . ((r . i),(I \; C)) ) by A31, A33, A34, ZFMISC_1:56; :: thesis:

end;

A35: [s,C] in TerminatingPrograms (A,S,T,f) by A28, ZFMISC_1:56;
A36: while (C,I) <> I \; J by A1, Th73;
A37: [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) by A29, A30, A32, A35, Def35;
[s,(while (C,I))] <> [s,(I \; J)] by A36, XTUPLE_0:1;
hence [s,(while (C,I))] in P by A37, ZFMISC_1:56; :: thesis:

end;

hereby :: thesis:

assume A38: [s,I] nin TerminatingPrograms (A,S,T,f) ; :: thesis:

let q be Element of S; :: thesis:
let C, I9, J9 be Element of A; :: thesis:
assume that
A39: [q,I9] in P and
A40: [(f . (q,I9)),J9] in P ; :: thesis:
A41: [q,I9] in TerminatingPrograms (A,S,T,f) by A39, ZFMISC_1:56;
A42: [(f . (q,I9)),J9] in TerminatingPrograms (A,S,T,f) by A40, ZFMISC_1:56;
A43: ( q <> s or I9 \; J9 <> I \; J ) by A1, A38, A41, Th73;
A44: [q,(I9 \; J9)] in TerminatingPrograms (A,S,T,f) by A41, A42, Def35;
[q,(I9 \; J9)] <> [s,(I \; J)] by A43, XTUPLE_0:1;
hence [q,(I9 \; J9)] in P by A44, ZFMISC_1:56; :: thesis:

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

end;

assume A45: [(f . (s,I)),J] nin TerminatingPrograms (A,S,T,f) ; :: thesis:

let q be Element of S; :: thesis:
let C, I9, J9 be Element of A; :: thesis:
assume that
A46: [q,I9] in P and
A47: [(f . (q,I9)),J9] in P ; :: thesis:
A48: [q,I9] in TerminatingPrograms (A,S,T,f) by A46, ZFMISC_1:56;
A49: [(f . (q,I9)),J9] in TerminatingPrograms (A,S,T,f) by A47, ZFMISC_1:56;
( f . (q,I9) <> f . (s,I) or J9 <> J ) by A45, A47, ZFMISC_1:56;
then A50: ( q <> s or I9 \; J9 <> I \; J ) by A1, Th73;
A51: [q,(I9 \; J9)] in TerminatingPrograms (A,S,T,f) by A48, A49, Def35;
[q,(I9 \; J9)] <> [s,(I \; J)] by A50, XTUPLE_0:1;
hence [q,(I9 \; J9)] in P by A51, ZFMISC_1:56; :: thesis:

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