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 A1: ( A is free & [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:] ;
A2: [:S,(ElementaryInstructions A):] c= P

let x, y be set ; :: according to RELAT_1:def 3 :: thesis:
assume A3: [x,y] in [:S,(ElementaryInstructions A):] ; :: thesis:
then ( I <> I \; J & J <> I \; J & y in ElementaryInstructions A ) by A1, Th73, ZFMISC_1:106;
then y <> I \; J by Th50;
then ( [:S,(ElementaryInstructions A):] c= TerminatingPrograms A,S,T,f & [x,y] <> [s,(I \; J)] ) by Def35, ZFMISC_1:33;
then ( [x,y] nin {[s,(I \; J)]} & [x,y] in TerminatingPrograms A,S,T,f ) by A3, TARSKI:def 1;
hence not [x,y] nin P by XBOOLE_0:def 5; :: thesis:

end;

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

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

end;

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

A6: now

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

hereby :: thesis:

assume A7: ( [s,C] in P & [(f . s,C),I] in P & f . s,C in T ) ; :: thesis:
then ( [s,C] in TerminatingPrograms A,S,T,f & [(f . s,C),I] in TerminatingPrograms A,S,T,f & I \; J <> if-then-else C,I,J ) by A1, Th73, ZFMISC_1:64;
then ( [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f & [s,(I \; J)] <> [s,(if-then-else C,I,J)] ) by A7, Def35, ZFMISC_1:33;
hence [s,(if-then-else C,I,J)] in P by ZFMISC_1:64; :: thesis:

end;

hereby :: thesis:

assume A8: ( [s,C] in P & [(f . s,C),J] in P & f . s,C nin T ) ; :: thesis:
then ( [s,C] in TerminatingPrograms A,S,T,f & [(f . s,C),J] in TerminatingPrograms A,S,T,f & I \; J <> if-then-else C,I,J ) by A1, Th73, ZFMISC_1:64;
then ( [s,(if-then-else C,I,J)] in TerminatingPrograms A,S,T,f & [s,(I \; J)] <> [s,(if-then-else C,I,J)] ) by A8, Def35, ZFMISC_1:33;
hence [s,(if-then-else C,I,J)] in P by ZFMISC_1:64; :: thesis:

end;

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

A12: now

let i be Nat; :: thesis:
assume ( 1 <= i & i < len r ) ; :: thesis:
then ( r . i in T & [(r . i),(I \; C)] in P & r . (i + 1) = f . (r . i),(I \; C) ) by A11;
hence ( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms A,S,T,f & r . (i + 1) = f . (r . i),(I \; C) ) by ZFMISC_1:64; :: thesis:

end;

( [s,C] in TerminatingPrograms A,S,T,f & while C,I <> I \; J ) by A1, Th73, A9, ZFMISC_1:64;
then ( [s,(while C,I)] in TerminatingPrograms A,S,T,f & [s,(while C,I)] <> [s,(I \; J)] ) by A10, A12, Def35, ZFMISC_1:33;
hence [s,(while C,I)] in P by ZFMISC_1:64; :: thesis:

end;

hereby :: thesis:

assume A13: [s,I] nin TerminatingPrograms A,S,T,f ; :: thesis:

let q be Element of S; :: thesis:
let C, I', J' be Element of A; :: thesis:
assume ( [q,I'] in P & [(f . q,I'),J'] in P ) ; :: thesis:
then A14: ( [q,I'] in TerminatingPrograms A,S,T,f & [(f . q,I'),J'] in TerminatingPrograms A,S,T,f ) by ZFMISC_1:64;
then ( q <> s or I' \; J' <> I \; J ) by A13, A1, Th73;
then ( [q,(I' \; J')] in TerminatingPrograms A,S,T,f & [q,(I' \; J')] <> [s,(I \; J)] ) by A14, Def35, ZFMISC_1:33;
hence [q,(I' \; J')] in P by ZFMISC_1:64; :: 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 A6;
then TerminatingPrograms A,S,T,f c= P by A2, A4, Def35;
hence contradiction by A1, ZFMISC_1:64; :: thesis:

end;

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

let q be Element of S; :: thesis:
let C, I', J' be Element of A; :: thesis:
assume A16: ( [q,I'] in P & [(f . q,I'),J'] in P ) ; :: thesis:
then A17: ( [q,I'] in TerminatingPrograms A,S,T,f & [(f . q,I'),J'] in TerminatingPrograms A,S,T,f ) by ZFMISC_1:64;
( f . q,I' <> f . s,I or J' <> J ) by A15, A16, ZFMISC_1:64;
then ( q <> s or I' \; J' <> I \; J ) by A1, Th73;
then ( [q,(I' \; J')] in TerminatingPrograms A,S,T,f & [q,(I' \; J')] <> [s,(I \; J)] ) by A17, Def35, ZFMISC_1:33;
hence [q,(I' \; J')] in P by ZFMISC_1:64; :: thesis:

end;