let A be preIfWhileAlgebra; :: thesis:
let C, 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);
set rr = s;
set IJ = if-then-else (C,I,J);
assume that
A1: A is free and
A2: [s,(if-then-else (C,I,J))] in TerminatingPrograms (A,S,T,f) ; :: thesis:
reconsider P = (TerminatingPrograms (A,S,T,f)) \ {[s,(if-then-else (C,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:
then y in ElementaryInstructions A by ZFMISC_1:87;
then A5: y <> if-then-else (C,I,J) by Th51;
A6: [:S,(ElementaryInstructions A):] c= TerminatingPrograms (A,S,T,f) by Def35;
[x,y] <> [s,(if-then-else (C,I,J))] by A5, XTUPLE_0:1;
then [x,y] nin {[s,(if-then-else (C,I,J))]} by TARSKI:def 1;
hence not [x,y] nin P by A4, A6, XBOOLE_0:def 5; :: thesis:

end;

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

let x, y be object ; :: according to RELAT_1:def 3 :: thesis:
assume A8: [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 A9: y <> if-then-else (C,I,J) by A1, Th72;
A10: [:S,{(EmptyIns A)}:] c= TerminatingPrograms (A,S,T,f) by Def35;
[x,y] <> [s,(if-then-else (C,I,J))] by A9, XTUPLE_0:1;
then [x,y] nin {[s,(if-then-else (C,I,J))]} by TARSKI:def 1;
hence not [x,y] nin P by A8, A10, XBOOLE_0:def 5; :: thesis:

end;

A11: now :: thesis:

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

hereby :: thesis:

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

end;

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

A22: now :: thesis:

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

end;

A25: [s,C] in TerminatingPrograms (A,S,T,f) by A18, ZFMISC_1:56;
A26: while (C,I) <> if-then-else (C,I,J) by A1, Th74;
A27: [s,(while (C,I))] in TerminatingPrograms (A,S,T,f) by A19, A20, A22, A25, Def35;
[s,(while (C,I))] <> [s,(if-then-else (C,I,J))] by A26, XTUPLE_0:1;
hence [s,(while (C,I))] in P by A27, ZFMISC_1:56; :: thesis:

end;

hereby :: thesis:

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

A29: now :: thesis:

let s be Element of S; :: thesis:
let C9, I, J be Element of A; :: thesis:
assume that
A30: [s,C9] in P and
A31: [(f . (s,C9)),I] in P and
A32: f . (s,C9) in T ; :: thesis:
A33: [s,C9] in TerminatingPrograms (A,S,T,f) by A30, ZFMISC_1:56;
A34: [(f . (s,C9)),I] in TerminatingPrograms (A,S,T,f) by A31, ZFMISC_1:56;
A35: ( if-then-else (C,I,J) <> if-then-else (C9,I,J) or s <> s ) by A1, A28, A33, Th74;
A36: [s,(if-then-else (C9,I,J))] in TerminatingPrograms (A,S,T,f) by A32, A33, A34, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I,J))] by A35, XTUPLE_0:1;
hence [s,(if-then-else (C9,I,J))] in P by A36, ZFMISC_1:56; :: thesis:

end;

let s be Element of S; :: thesis:
let C9, I, J be Element of A; :: thesis:
assume that
A37: [s,C9] in P and
A38: [(f . (s,C9)),J] in P and
A39: f . (s,C9) nin T ; :: thesis:
A40: [s,C9] in TerminatingPrograms (A,S,T,f) by A37, ZFMISC_1:56;
A41: [(f . (s,C9)),J] in TerminatingPrograms (A,S,T,f) by A38, ZFMISC_1:56;
A42: ( if-then-else (C,I,J) <> if-then-else (C9,I,J) or s <> s ) by A1, A28, A40, Th74;
A43: [s,(if-then-else (C9,I,J))] in TerminatingPrograms (A,S,T,f) by A39, A40, A41, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I,J))] by A42, XTUPLE_0:1;
hence [s,(if-then-else (C9,I,J))] in P by A43, ZFMISC_1:56; :: thesis:

end;

then TerminatingPrograms (A,S,T,f) c= P by A3, A7, A11, A29, Def35;
hence contradiction by A2, ZFMISC_1:56; :: thesis:

end;

thus ( f . (s,C) in T implies [(f . (s,C)),I] in TerminatingPrograms (A,S,T,f) ) :: thesis:

assume that
A44: f . (s,C) in T and
A45: [(f . (s,C)),I] nin TerminatingPrograms (A,S,T,f) ; :: thesis:

A46: now :: thesis:

let s be Element of S; :: thesis:
let C9, I9, J be Element of A; :: thesis:
assume that
A47: [s,C9] in P and
A48: [(f . (s,C9)),I9] in P and
A49: f . (s,C9) in T ; :: thesis:
A50: [s,C9] in TerminatingPrograms (A,S,T,f) by A47, ZFMISC_1:56;
A51: [(f . (s,C9)),I9] in TerminatingPrograms (A,S,T,f) by A48, ZFMISC_1:56;
( f . (s,C9) <> f . (s,C) or I <> I9 ) by A45, A48, ZFMISC_1:56;
then A52: ( if-then-else (C,I,J) <> if-then-else (C9,I9,J) or s <> s ) by A1, Th74;
A53: [s,(if-then-else (C9,I9,J))] in TerminatingPrograms (A,S,T,f) by A49, A50, A51, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I9,J))] by A52, XTUPLE_0:1;
hence [s,(if-then-else (C9,I9,J))] in P by A53, ZFMISC_1:56; :: thesis:

end;

let s be Element of S; :: thesis:
let C9, I, J9 be Element of A; :: thesis:
assume that
A54: [s,C9] in P and
A55: [(f . (s,C9)),J9] in P and
A56: f . (s,C9) nin T ; :: thesis:
A57: [s,C9] in TerminatingPrograms (A,S,T,f) by A54, ZFMISC_1:56;
A58: [(f . (s,C9)),J9] in TerminatingPrograms (A,S,T,f) by A55, ZFMISC_1:56;
A59: ( if-then-else (C,I,J) <> if-then-else (C9,I,J9) or s <> s ) by A1, A44, A56, Th74;
A60: [s,(if-then-else (C9,I,J9))] in TerminatingPrograms (A,S,T,f) by A56, A57, A58, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I,J9))] by A59, XTUPLE_0:1;
hence [s,(if-then-else (C9,I,J9))] in P by A60, ZFMISC_1:56; :: thesis:

end;

then TerminatingPrograms (A,S,T,f) c= P by A3, A7, A11, A46, Def35;
hence contradiction by A2, ZFMISC_1:56; :: thesis:

end;

assume that
A61: f . (s,C) nin T and
A62: [(f . (s,C)),J] nin TerminatingPrograms (A,S,T,f) ; :: thesis:

A63: now :: thesis:

let s be Element of S; :: thesis:
let C9, I9, J be Element of A; :: thesis:
assume that
A64: [s,C9] in P and
A65: [(f . (s,C9)),I9] in P and
A66: f . (s,C9) in T ; :: thesis:
A67: [s,C9] in TerminatingPrograms (A,S,T,f) by A64, ZFMISC_1:56;
A68: [(f . (s,C9)),I9] in TerminatingPrograms (A,S,T,f) by A65, ZFMISC_1:56;
A69: ( if-then-else (C,I,J) <> if-then-else (C9,I9,J) or s <> s ) by A1, A61, A66, Th74;
A70: [s,(if-then-else (C9,I9,J))] in TerminatingPrograms (A,S,T,f) by A66, A67, A68, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I9,J))] by A69, XTUPLE_0:1;
hence [s,(if-then-else (C9,I9,J))] in P by A70, ZFMISC_1:56; :: thesis:

end;

let s be Element of S; :: thesis:
let C9, I, J9 be Element of A; :: thesis:
assume that
A71: [s,C9] in P and
A72: [(f . (s,C9)),J9] in P and
A73: f . (s,C9) nin T ; :: thesis:
A74: [s,C9] in TerminatingPrograms (A,S,T,f) by A71, ZFMISC_1:56;
A75: [(f . (s,C9)),J9] in TerminatingPrograms (A,S,T,f) by A72, ZFMISC_1:56;
( f . (s,C9) <> f . (s,C) or J <> J9 ) by A62, A72, ZFMISC_1:56;
then A76: ( if-then-else (C,I,J) <> if-then-else (C9,I,J9) or s <> s ) by A1, Th74;
A77: [s,(if-then-else (C9,I,J9))] in TerminatingPrograms (A,S,T,f) by A73, A74, A75, Def35;
[s,(if-then-else (C,I,J))] <> [s,(if-then-else (C9,I,J9))] by A76, XTUPLE_0:1;
hence [s,(if-then-else (C9,I,J9))] in P by A77, ZFMISC_1:56; :: thesis:

end;

then TerminatingPrograms (A,S,T,f) c= P by A3, A7, A11, A63, Def35;
hence contradiction by A2, ZFMISC_1:56; :: thesis: