let S be non empty set ; for T being Subset of S
for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
let T be Subset of S; for A being free ECIW-strict preIfWhileAlgebra
for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
let A be free ECIW-strict preIfWhileAlgebra; for f1, f2 being ExecutionFunction of A,S,T st f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] holds
for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
let f1, f2 be ExecutionFunction of A,S,T; ( f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] implies for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) ) )
assume A1:
f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):]
; for I being Element of A
for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
set g = f1 | [:S,(ElementaryInstructions A):];
set TP1 = TerminatingPrograms (A,S,T,f1);
set TP2 = TerminatingPrograms (A,S,T,f2);
defpred S1[ Element of A] means for s being Element of S st [s,$1] in TerminatingPrograms (A,S,T,f1) holds
( [s,$1] in TerminatingPrograms (A,S,T,f2) & f1 . (s,$1) = f2 . (s,$1) );
A2:
for I being Element of A st I in ElementaryInstructions A holds
S1[I]
proof
let I be
Element of
A;
( I in ElementaryInstructions A implies S1[I] )
assume A3:
I in ElementaryInstructions A
;
S1[I]
let s be
Element of
S;
( [s,I] in TerminatingPrograms (A,S,T,f1) implies ( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) ) )
assume
[s,I] in TerminatingPrograms (
A,
S,
T,
f1)
;
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
thus
[s,I] in TerminatingPrograms (
A,
S,
T,
f2)
by A3, Th94;
f1 . (s,I) = f2 . (s,I)
A4:
[s,I] in [:S,(ElementaryInstructions A):]
by A3, ZFMISC_1:87;
hence f1 . (
s,
I) =
(f1 | [:S,(ElementaryInstructions A):]) . [s,I]
by FUNCT_1:49
.=
f2 . (
s,
I)
by A1, A4, FUNCT_1:49
;
verum
end;
A5:
S1[ EmptyIns A]
proof
let s be
Element of
S;
( [s,(EmptyIns A)] in TerminatingPrograms (A,S,T,f1) implies ( [s,(EmptyIns A)] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(EmptyIns A)) = f2 . (s,(EmptyIns A)) ) )
f1 . (
s,
(EmptyIns A))
= s
by Def28;
hence
(
[s,(EmptyIns A)] in TerminatingPrograms (
A,
S,
T,
f1) implies (
[s,(EmptyIns A)] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
s,
(EmptyIns A))
= f2 . (
s,
(EmptyIns A)) ) )
by Def28, Th96;
verum
end;
A6:
for I1, I2 being Element of A st S1[I1] & S1[I2] holds
S1[I1 \; I2]
proof
let I1,
I2 be
Element of
A;
( S1[I1] & S1[I2] implies S1[I1 \; I2] )
assume that A7:
S1[
I1]
and A8:
S1[
I2]
;
S1[I1 \; I2]
let s be
Element of
S;
( [s,(I1 \; I2)] in TerminatingPrograms (A,S,T,f1) implies ( [s,(I1 \; I2)] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(I1 \; I2)) = f2 . (s,(I1 \; I2)) ) )
assume A9:
[s,(I1 \; I2)] in TerminatingPrograms (
A,
S,
T,
f1)
;
( [s,(I1 \; I2)] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(I1 \; I2)) = f2 . (s,(I1 \; I2)) )
then A10:
[s,I1] in TerminatingPrograms (
A,
S,
T,
f1)
by Th97;
A11:
[(f1 . (s,I1)),I2] in TerminatingPrograms (
A,
S,
T,
f1)
by A9, Th97;
A12:
[s,I1] in TerminatingPrograms (
A,
S,
T,
f2)
by A7, A10;
A13:
[(f1 . (s,I1)),I2] in TerminatingPrograms (
A,
S,
T,
f2)
by A8, A11;
A14:
f1 . (
s,
I1)
= f2 . (
s,
I1)
by A7, A10;
A15:
f1 . (
(f1 . (s,I1)),
I2)
= f2 . (
(f1 . (s,I1)),
I2)
by A8, A11;
f1 . (
(f1 . (s,I1)),
I2)
= f1 . (
s,
(I1 \; I2))
by Def29;
hence
(
[s,(I1 \; I2)] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
s,
(I1 \; I2))
= f2 . (
s,
(I1 \; I2)) )
by A12, A13, A14, A15, Def29, Def35;
verum
end;
A16:
for C, I1, I2 being Element of A st S1[C] & S1[I1] & S1[I2] holds
S1[ if-then-else (C,I1,I2)]
proof
let C,
I1,
I2 be
Element of
A;
( S1[C] & S1[I1] & S1[I2] implies S1[ if-then-else (C,I1,I2)] )
assume that A17:
S1[
C]
and A18:
S1[
I1]
and A19:
S1[
I2]
;
S1[ if-then-else (C,I1,I2)]
A20:
f1 complies_with_if_wrt T
by Def32;
A21:
f2 complies_with_if_wrt T
by Def32;
set J =
if-then-else (
C,
I1,
I2);
let s be
Element of
S;
( [s,(if-then-else (C,I1,I2))] in TerminatingPrograms (A,S,T,f1) implies ( [s,(if-then-else (C,I1,I2))] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(if-then-else (C,I1,I2))) = f2 . (s,(if-then-else (C,I1,I2))) ) )
assume A22:
[s,(if-then-else (C,I1,I2))] in TerminatingPrograms (
A,
S,
T,
f1)
;
( [s,(if-then-else (C,I1,I2))] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(if-then-else (C,I1,I2))) = f2 . (s,(if-then-else (C,I1,I2))) )
then A23:
[s,C] in TerminatingPrograms (
A,
S,
T,
f1)
by Th98;
A24:
(
f1 . (
s,
C)
in T implies
[(f1 . (s,C)),I1] in TerminatingPrograms (
A,
S,
T,
f1) )
by A22, Th98;
A25:
(
f1 . (
s,
C)
nin T implies
[(f1 . (s,C)),I2] in TerminatingPrograms (
A,
S,
T,
f1) )
by A22, Th98;
A26:
[s,C] in TerminatingPrograms (
A,
S,
T,
f2)
by A17, A23;
A27:
f1 . (
s,
C)
= f2 . (
s,
C)
by A17, A23;
A28:
(
f1 . (
s,
C)
in T implies (
[(f1 . (s,C)),I1] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
(f1 . (s,C)),
I1)
= f2 . (
(f1 . (s,C)),
I1) &
f1 . (
s,
(if-then-else (C,I1,I2)))
= f1 . (
(f1 . (s,C)),
I1) ) )
by A18, A20, A24;
A29:
(
f1 . (
s,
C)
nin T implies (
[(f1 . (s,C)),I2] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
(f1 . (s,C)),
I2)
= f2 . (
(f1 . (s,C)),
I2) &
f1 . (
s,
(if-then-else (C,I1,I2)))
= f1 . (
(f1 . (s,C)),
I2) ) )
by A19, A20, A25;
(
f1 . (
s,
C)
in T or
f1 . (
s,
C)
nin T )
;
hence
(
[s,(if-then-else (C,I1,I2))] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
s,
(if-then-else (C,I1,I2)))
= f2 . (
s,
(if-then-else (C,I1,I2))) )
by A21, A26, A27, A28, A29, Def35;
verum
end;
A30:
for C, I being Element of A st S1[C] & S1[I] holds
S1[ while (C,I)]
proof
let C,
I be
Element of
A;
( S1[C] & S1[I] implies S1[ while (C,I)] )
assume that A31:
S1[
C]
and A32:
S1[
I]
;
S1[ while (C,I)]
set J =
while (
C,
I);
let s be
Element of
S;
( [s,(while (C,I))] in TerminatingPrograms (A,S,T,f1) implies ( [s,(while (C,I))] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) ) )
assume A33:
[s,(while (C,I))] in TerminatingPrograms (
A,
S,
T,
f1)
;
( [s,(while (C,I))] in TerminatingPrograms (A,S,T,f2) & f1 . (s,(while (C,I))) = f2 . (s,(while (C,I))) )
then A34:
[s,C] in TerminatingPrograms (
A,
S,
T,
f1)
by Th99;
then A35:
[s,C] in TerminatingPrograms (
A,
S,
T,
f2)
by A31;
A36:
f1 . (
s,
C)
= f2 . (
s,
C)
by A31, A34;
consider r being non
empty FinSequence of
S such that A37:
r . 1
= f1 . (
s,
C)
and A38:
r . (len r) nin T
and A39:
for
i being
Nat st 1
<= i &
i < len r holds
(
r . i in T &
[(r . i),(I \; C)] in TerminatingPrograms (
A,
S,
T,
f1) &
r . (i + 1) = f1 . (
(r . i),
(I \; C)) )
by A33, Th99;
for
i being
Nat st 1
<= i &
i < len r holds
(
r . i in T &
r . (i + 1) = f1 . (
(r . i),
(I \; C)) )
by A39;
then A40:
f1 . (
s,
(while (C,I)))
= r . (len r)
by A37, A38, Th86;
defpred S2[
Nat]
means ( 1
<= $1 & $1
< len r implies (
r . $1
in T &
[(r . $1),(I \; C)] in TerminatingPrograms (
A,
S,
T,
f2) &
r . ($1 + 1) = f2 . (
(r . $1),
(I \; C)) ) );
A41:
for
i being
Nat holds
S2[
i]
proof
let i be
Nat;
S2[i]
assume that A42:
1
<= i
and A43:
i < len r
;
( r . i in T & [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f2) & r . (i + 1) = f2 . ((r . i),(I \; C)) )
thus A44:
r . i in T
by A39, A42, A43;
( [(r . i),(I \; C)] in TerminatingPrograms (A,S,T,f2) & r . (i + 1) = f2 . ((r . i),(I \; C)) )
then reconsider ri =
r . i as
Element of
S ;
A45:
[(r . i),(I \; C)] in TerminatingPrograms (
A,
S,
T,
f1)
by A39, A42, A43;
hence
[(r . i),(I \; C)] in TerminatingPrograms (
A,
S,
T,
f2)
by A6, A31, A32, A44;
r . (i + 1) = f2 . ((r . i),(I \; C))
A46:
[ri,I] in TerminatingPrograms (
A,
S,
T,
f1)
by A45, Th97;
A47:
[(f1 . (ri,I)),C] in TerminatingPrograms (
A,
S,
T,
f1)
by A45, Th97;
thus r . (i + 1) =
f1 . (
(r . i),
(I \; C))
by A39, A42, A43
.=
f1 . (
(f1 . (ri,I)),
C)
by Def29
.=
f2 . (
(f1 . (ri,I)),
C)
by A31, A47
.=
f2 . (
(f2 . (ri,I)),
C)
by A32, A46
.=
f2 . (
(r . i),
(I \; C))
by Def29
;
verum
end;
then
for
i being
Nat st 1
<= i &
i < len r holds
(
r . i in T &
r . (i + 1) = f2 . (
(r . i),
(I \; C)) )
;
hence
(
[s,(while (C,I))] in TerminatingPrograms (
A,
S,
T,
f2) &
f1 . (
s,
(while (C,I)))
= f2 . (
s,
(while (C,I))) )
by A35, A36, A37, A38, A40, A41, Def35, Th86;
verum
end;
let I be Element of A; for s being Element of S st [s,I] in TerminatingPrograms (A,S,T,f1) holds
( [s,I] in TerminatingPrograms (A,S,T,f2) & f1 . (s,I) = f2 . (s,I) )
thus
S1[I]
from AOFA_000:sch 2(A2, A5, A6, A16, A30); verum