let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; for X being V3() ManySortedSet of the carrier of S
for T being non-empty b1,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let X be V3() ManySortedSet of the carrier of S; for T being non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S
for C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; for C being bool-correct 4,1 integer 11,1,1 -array image of T
for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let C be bool-correct 4,1 integer 11,1,1 -array image of T; for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let G be basic GeneratorSystem over S,X,T; for I being integer SortSymbol of S
for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let I be integer SortSymbol of S; for m, i being pure Element of the generators of G . I
for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let m, i be pure Element of the generators of G . I; for M being pure Element of the generators of G . (the_array_sort_of S)
for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let M be pure Element of the generators of G . (the_array_sort_of S); for b being pure Element of the generators of G . the bool-sort of S
for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let b be pure Element of the generators of G . the bool-sort of S; for A being elementary IfWhileAlgebra of the generators of G
for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let A be elementary IfWhileAlgebra of the generators of G; for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m holds
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); ( f in C -Execution (A,b,(\false C)) & G is C -supported & i <> m implies (m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume A1:
f in C -Execution (A,b,(\false C))
; ( not G is C -supported or not i <> m or (m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume A2:
G is C -supported
; ( not i <> m or (m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume A3:
i <> m
; (m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
set J = m := ((\0 (T,I)),A);
set K = i := ((\1 (T,I)),A);
set W = b gt ((length ((@ M),I)),(@ i),A);
set L = i := (((@ i) + (\1 (T,I))),A);
set N = b gt (((@ M) . (@ i)),((@ M) . (@ m)),A);
set O = m := ((@ i),A);
set a = the_array_sort_of S;
set P = { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } ;
A4:
( the Sorts of C . the bool-sort of S = BOOLEAN & the Sorts of C . (the_array_sort_of S) = INT ^omega )
by Th74, AOFA_A00:def 32;
then A5:
( the bool-sort of S <> the_array_sort_of S & I <> the_array_sort_of S & the bool-sort of S <> I )
by Th73, AOFA_A00:53;
A6:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt m := ((\0 (T,I)),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(m := ((\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(m := ((\0 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A7:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(m := ((\0 (T,I)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A5, Th65;
hence
f . (
s,
(m := ((\0 (T,I)),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A7;
verum
end;
A8:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt i := ((\1 (T,I)),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(i := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(i := ((\1 (T,I)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A9:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(i := ((\1 (T,I)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A5, Th65;
hence
f . (
s,
(i := ((\1 (T,I)),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A9;
verum
end;
A10:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt b gt ((length ((@ M),I)),(@ i),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(b gt ((length ((@ M),I)),(@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A11:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A4, Th65;
hence
f . (
s,
(b gt ((length ((@ M),I)),(@ i),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A11;
verum
end;
A12:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt i := (((@ i) + (\1 (T,I))),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(i := (((@ i) + (\1 (T,I))),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(i := (((@ i) + (\1 (T,I))),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A13:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(i := (((@ i) + (\1 (T,I))),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A5, Th65;
hence
f . (
s,
(i := (((@ i) + (\1 (T,I))),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A13;
verum
end;
A14:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt b gt (((@ M) . (@ i)),((@ M) . (@ m)),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A15:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A4, Th65;
hence
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A15;
verum
end;
A16:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt m := ((@ i),A),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(m := ((@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(m := ((@ i),A))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then consider s1 being
Element of
C -States the
generators of
G such that A17:
(
s = s1 &
(s1 . (the_array_sort_of S)) . M <> {} )
;
((f . (s,(m := ((@ i),A)))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . M
by A1, A2, A5, Th65;
hence
f . (
s,
(m := ((@ i),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A17;
verum
end;
set ST = C -States the generators of G;
set TV = (\false C) -States ( the generators of G,b);
A18:
f complies_with_if_wrt (\false C) -States ( the generators of G,b)
by AOFA_000:def 32;
A19:
{ s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } is_invariant_wrt if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))),f
proof
let s be
Element of
C -States the
generators of
G;
AOFA_000:def 39 ( not s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } or f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } )
assume
s in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
;
f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
then A20:
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A14;
per cases
( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) )
;
suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
in (\false C) -States ( the
generators of
G,
b)
;
f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } then
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(m := ((@ i),A)))
by A18;
hence
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A20, A16;
verum end; suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
nin (\false C) -States ( the
generators of
G,
b)
;
f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} } then
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(EmptyIns A))
by A18;
hence
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
in { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A20, AOFA_000:def 28;
verum end; end;
end;
A21:
m := ((\0 (T,I)),A) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by AOFA_000:107;
for s being Element of C -States the generators of G holds
( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i & (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = (length ((@ M),I)) value_at (C,s) & (length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = (length ((@ M),I)) value_at (C,s) )
proof
let s be
Element of
C -States the
generators of
G;
( ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . i & ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i & (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = (length ((@ M),I)) value_at (C,s) & (length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = (length ((@ M),I)) value_at (C,s) )
hereby ( ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i & (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = (length ((@ M),I)) value_at (C,s) & (length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = (length ((@ M),I)) value_at (C,s) )
per cases
( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) )
;
suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
in (\false C) -States ( the
generators of
G,
b)
;
((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . ithen
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(m := ((@ i),A)))
by A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i =
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i
by A1, A2, A3, Th65
.=
(s . I) . i
by A1, A2, A5, Th65
;
verum end; suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
nin (\false C) -States ( the
generators of
G,
b)
;
((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i = (s . I) . ithen
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(EmptyIns A))
by A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . I) . i =
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . I) . i
by AOFA_000:def 28
.=
(s . I) . i
by A1, A2, A5, Th65
;
verum end; end;
end;
A22:
now ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . Mper cases
( f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) in (\false C) -States ( the generators of G,b) or f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A))) nin (\false C) -States ( the generators of G,b) )
;
suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
in (\false C) -States ( the
generators of
G,
b)
;
((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . Mthen
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(m := ((@ i),A)))
by A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M =
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M
by A1, A2, A5, Th65
.=
(s . (the_array_sort_of S)) . M
by A1, A2, A4, Th65
;
verum end; suppose
f . (
s,
(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))
nin (\false C) -States ( the
generators of
G,
b)
;
((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M = (s . (the_array_sort_of S)) . Mthen
f . (
s,
(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))
= f . (
(f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))),
(EmptyIns A))
by A18;
hence ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M =
((f . (s,(b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)))) . (the_array_sort_of S)) . M
by AOFA_000:def 28
.=
(s . (the_array_sort_of S)) . M
by A1, A2, A4, Th65
;
verum end; end; end;
thus
((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . I) . i = (s . I) . i
by A1, A2, A5, Th65;
( (length ((@ M),I)) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) = (length ((@ M),I)) value_at (C,s) & (length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = (length ((@ M),I)) value_at (C,s) )
A23:
(
(@ M) value_at (
C,
(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))
= ((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . (the_array_sort_of S)) . M &
(@ M) value_at (
C,
(f . (s,(b gt ((length ((@ M),I)),(@ i),A)))))
= ((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M &
(@ M) value_at (
C,
s)
= (s . (the_array_sort_of S)) . M )
by Th61;
thus (length ((@ M),I)) value_at (
C,
(f . (s,(b gt ((length ((@ M),I)),(@ i),A))))) =
length (
((@ M) value_at (C,(f . (s,(b gt ((length ((@ M),I)),(@ i),A)))))),
I)
by Th81
.=
len (((f . (s,(b gt ((length ((@ M),I)),(@ i),A)))) . (the_array_sort_of S)) . M)
by A23, Th74
.=
len ((s . (the_array_sort_of S)) . M)
by A1, A2, A4, Th65
.=
length (
((@ M) value_at (C,s)),
I)
by A23, Th74
.=
(length ((@ M),I)) value_at (
C,
s)
by Th81
;
(length ((@ M),I)) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) = (length ((@ M),I)) value_at (C,s)
thus (length ((@ M),I)) value_at (
C,
(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A)))))) =
length (
((@ M) value_at (C,(f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))))),
I)
by Th81
.=
len (((f . (s,((if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))) \; (i := (((@ i) + (\1 (T,I))),A))))) . (the_array_sort_of S)) . M)
by A23, Th74
.=
len (((f . ((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))),(i := (((@ i) + (\1 (T,I))),A)))) . (the_array_sort_of S)) . M)
by AOFA_000:def 29
.=
len (((f . (s,(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) . (the_array_sort_of S)) . M)
by A1, A2, A5, Th65
.=
length (
((@ M) value_at (C,s)),
I)
by A23, A22, Th74
.=
(length ((@ M),I)) value_at (
C,
s)
by Th81
;
verum
end;
then
for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A1, A2, A8, A10, A12, A19, Th94, AOFA_000:107;
hence
(m := ((\0 (T,I)),A)) \; (for-do ((i := ((\1 (T,I)),A)),(b gt ((length ((@ M),I)),(@ i),A)),(i := (((@ i) + (\1 (T,I))),A)),(if-then ((b gt (((@ M) . (@ i)),((@ M) . (@ m)),A)),(m := ((@ i),A)))))) is_terminating_wrt f, { s where s is Element of C -States the generators of G : (s . (the_array_sort_of S)) . M <> {} }
by A6, A21, AOFA_000:111; verum