let A be preIfWhileAlgebra; 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; 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 ; 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; 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; 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; ( 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)
; ( [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 ;
RELAT_1:def 3 ( [x,y] nin [:S,(ElementaryInstructions A):] or not [x,y] nin P )
assume A4:
[x,y] in [:S,(ElementaryInstructions A):]
;
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;
verum
end;
A7:
[:S,{(EmptyIns A)}:] c= P
proof
let x,
y be
object ;
RELAT_1:def 3 ( [x,y] nin [:S,{(EmptyIns A)}:] or not [x,y] nin P )
assume A8:
[x,y] in [:S,{(EmptyIns A)}:]
;
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;
verum
end;
A11:
now 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;
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;
( ( [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 ( ( [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
;
[s,(I \; J)] in PA14:
[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;
verum
end; hereby ( [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
;
[s,(if-then-else (C,I,J))] in PA21:
[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;
verum
end; hereby verum
assume that A25:
[s,C] in P
and A26:
[(f . (s,C)),J] in P
and A27:
f . (
s,
C)
nin T
;
[s,(if-then-else (C,I,J))] in PA28:
[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;
verum
end; end;
hereby 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)
;
contradictionnow 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 Plet s be
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 Plet C9,
I9,
J be
Element of
A;
( [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
;
( 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)) )
;
[s,(while (C9,I9))] in PA37:
now 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;
( 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
;
( 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;
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;
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;
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)) ) ) )
; contradiction
now 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 Plet s be
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 Plet C9,
I9,
J be
Element of
A;
( [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
;
( 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)) )
;
[s,(while (C9,I9))] in PA48:
now 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;
( 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
;
( 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;
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;
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; verum