let S be non empty non void 1-1-connectives bool-correct 4,1 integer 11,1,1 -array 11 array-correct BoolSignature ; :: thesis: 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 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let X be V3() ManySortedSet of the carrier of S; :: thesis: 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 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let T be non-empty X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer-array VarMSAlgebra over S; :: thesis: 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 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let C be bool-correct 4,1 integer 11,1,1 -array image of T; :: thesis: for G being basic GeneratorSystem over S,X,T
for I being integer SortSymbol of S
for 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let G be basic GeneratorSystem over S,X,T; :: thesis: for I being integer SortSymbol of S
for 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let I be integer SortSymbol of S; :: thesis: for 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let i be pure Element of the generators of G . I; :: thesis: 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 s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let M be pure Element of the generators of G . (the_array_sort_of S); :: thesis: for b being pure Element of the generators of G . the bool-sort of S
for s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let b be pure Element of the generators of G . the bool-sort of S; :: thesis: for s being Element of C -States the generators of G
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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let s be Element of C -States the generators of G; :: thesis: 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 G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let A be elementary IfWhileAlgebra of the generators of G; :: thesis: for f being ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b) st G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated holds
for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let f be ExecutionFunction of A,C -States the generators of G,(\false C) -States ( the generators of G,b); :: thesis: ( G is integer-array & G is C -supported & f in C -Execution (A,b,(\false C)) & X is countable & not T is array-degenerated implies for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) )
assume A1: G is integer-array ; :: thesis: ( not G is C -supported or not f in C -Execution (A,b,(\false C)) or not X is countable or T is array-degenerated or for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) )
assume A2: G is C -supported ; :: thesis: ( not f in C -Execution (A,b,(\false C)) or not X is countable or T is array-degenerated or for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) )
assume A3: f in C -Execution (A,b,(\false C)) ; :: thesis: ( not X is countable or T is array-degenerated or for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) )
assume A4: X is countable ; :: thesis: ( T is array-degenerated or for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) )
assume A5: not T is array-degenerated ; :: thesis: for t being Element of T,I holds f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
let t be Element of T,I; :: thesis: f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A)))
reconsider H = FreeGen T as ManySortedSubset of the generators of G by Def3, PBOOLE:def 18;
set v = t value_at (C,s);
reconsider p = (@ M) . (@ i) as Element of G,I by A1, Th96, AOFA_A00:def 22;
reconsider g = s as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
reconsider g1 = f . (s,(((@ M) . (@ i)) := (t,A))), g2 = f . (s,(M := ((((@ M),(@ i)) <- t),A))) as ManySortedFunction of the generators of G, the Sorts of C by AOFA_A00:48;
reconsider Mi = (@ M) . (@ i) as Element of the generators of G . I by A1, Th96;
( M in the generators of G . (the_array_sort_of S) & the generators of G . (the_array_sort_of S) c= the Sorts of T . (the_array_sort_of S) ) by PBOOLE:def 2, PBOOLE:def 18;
then reconsider m = M as Element of G, the_array_sort_of S by AOFA_A00:def 22;
Mi := (t,A) = ((@ M) . (@ i)) := (t,A) by Def19;
then A6: ( g1 = succ (s,p,(t value_at (C,s))) & g2 = succ (s,m,((((@ M),(@ i)) <- t) value_at (C,s))) ) by A3, AOFA_A00:def 28;
A7: vf p = ((the_array_sort_of S) -singleton M) (\/) (I -singleton i) by A5, Th98;
M in (FreeGen T) . (the_array_sort_of S) by Def4;
then A8: vf (@ M) = (the_array_sort_of S) -singleton M by AOFA_A00:41;
i in (FreeGen T) . I by Def4;
then A9: vf (@ i) = I -singleton i by AOFA_A00:41;
consider x being pure Element of the generators of G . I such that
A10: ( x nin (vf (@ i)) . I & supp-var p = x & ((supp-term p) . (the_array_sort_of S)) . M = ((@ M),(@ i)) <- (@ x) & ( for s being SortSymbol of S
for y being pure Element of the generators of G . I st y in (vf p) . s & ( s = the_array_sort_of S implies y <> M ) holds
((supp-term p) . s) . y = y ) ) by A1;
g1 = g2
proof
let a be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: g1 . a = g2 . a
A11: now :: thesis: for a being SortSymbol of S
for b being Element of the generators of G . a st b in (FreeGen T) . a holds
(g1 . a) . b = (g2 . a) . b
let a be SortSymbol of S; :: thesis: for b being Element of the generators of G . a st b in (FreeGen T) . a holds
(g1 . b2) . b3 = (g2 . b2) . b3
A12: (vf (@ M)) . a c= (vf p) . a by A7, A8, PBOOLE:14, PBOOLE:def 2;
let b be Element of the generators of G . a; :: thesis: ( b in (FreeGen T) . a implies (g1 . b1) . b2 = (g2 . b1) . b2 )
assume A13: b in (FreeGen T) . a ; :: thesis: (g1 . b1) . b2 = (g2 . b1) . b2
per cases ( ( b in (FreeGen T) . a & b nin (vf p) . a ) or ( b in (FreeGen T) . a & b in (vf p) . a & b nin (vf (@ M)) . a ) or ( b in (FreeGen T) . a & b in (vf p) . a & b in (vf (@ M)) . a ) ) by A13;
suppose A14: ( b in (FreeGen T) . a & b nin (vf p) . a ) ; :: thesis: (g1 . b1) . b2 = (g2 . b1) . b2
then A15: b nin (vf (@ M)) . a by A12;
A16: now :: thesis: ( a = the_array_sort_of S implies b <> m )
assume a = the_array_sort_of S ; :: thesis: b <> m
then (vf (@ M)) . a = {M} by A8, AOFA_A00:6;
hence b <> m by A15, TARSKI:def 1; :: thesis: verum
end;
b is pure by A14;
then ( a = I implies b <> p ) by A4, Th97;
then ( (g1 . a) . b = (s . a) . b & (g2 . a) . b = (s . a) . b ) by A2, A6, A14, A15, A16, AOFA_A00:def 27;
hence (g1 . a) . b = (g2 . a) . b ; :: thesis: verum
end;
suppose A17: ( b in (FreeGen T) . a & b in (vf p) . a & b nin (vf (@ M)) . a ) ; :: thesis: (g1 . b1) . b2 = (g2 . b1) . b2
A18: now :: thesis: ( a = the_array_sort_of S implies b <> m )
assume a = the_array_sort_of S ; :: thesis: b <> m
then (vf (@ M)) . a = {M} by A8, AOFA_A00:6;
hence b <> m by A17, TARSKI:def 1; :: thesis: verum
end;
consider u being ManySortedFunction of FreeGen T, the Sorts of C such that
A19: u = (g || H) +* (I,(supp-var p),(t value_at (C,s))) ;
A20: ( ( a = I & b = i ) or ( a = the_array_sort_of S & b = M ) ) by A7, A17, Th4;
A21: ((supp-term p) . a) . b = @ i by A20, A17, A18, A10;
A22: i in (vf (@ i)) . a by A20, A8, A17, Th3, A9;
b is pure by A17;
then ( a = I implies b <> p ) by A4, Th97;
then (g1 . a) . b = (@ i) value_at (C,u) by A2, A6, A17, A19, A20, A21, A8, Th3, AOFA_A00:def 27
.= (u . a) . i by A20, A8, A17, Th3, Th62
.= (((g || H) . a) +* ((supp-var p),(t value_at (C,s)))) . b by A19, A20, A8, A17, Th3, AOFA_A00:def 2
.= ((g || H) . a) . b by A20, A22, A10, A8, A17, Th3, FUNCT_7:32
.= ((g . a) | (H . a)) . b by MSAFREE:def 1
.= (g . a) . b by A17, FUNCT_1:49 ;
hence (g1 . a) . b = (g2 . a) . b by A2, A6, A17, A18, AOFA_A00:def 27; :: thesis: verum
end;
suppose A23: ( b in (FreeGen T) . a & b in (vf p) . a & b in (vf (@ M)) . a ) ; :: thesis: (g1 . b1) . b2 = (g2 . b1) . b2
then A24: ( b = M & a = the_array_sort_of S ) by A8, Th3;
A25: I <> the_array_sort_of S by Th73;
set u = (g || H) +* (I,(supp-var p),(t value_at (C,s)));
reconsider uIx = (((g || H) +* (I,(supp-var p),(t value_at (C,s)))) . I) . x as Element of C,I by Def4, FUNCT_2:5;
A26: dom ((g || H) . I) = (FreeGen T) . I by FUNCT_2:def 1;
(vf (@ i)) . I = {i} by A9, AOFA_A00:6;
then A27: i in (vf (@ i)) . I by TARSKI:def 1;
A28: uIx = (((g || H) . I) +* (x,(t value_at (C,s)))) . x by A10, AOFA_A00:def 2
.= t value_at (C,s) by Def4, A26, FUNCT_7:31 ;
A29: (@ M) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s))))) = (((g || H) +* (I,(supp-var p),(t value_at (C,s)))) . (the_array_sort_of S)) . M by Th62
.= ((g || H) . a) . b by A24, A25, AOFA_A00:def 2
.= ((g . a) | (H . a)) . b by MSAFREE:def 1
.= (g . a) . b by A23, FUNCT_1:49
.= (@ M) value_at (C,s) by A24, Th61 ;
A30: (@ i) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s))))) = (((g || H) +* (I,(supp-var p),(t value_at (C,s)))) . I) . i by Th62
.= (((g || H) . I) +* (x,(t value_at (C,s)))) . i by A10, AOFA_A00:def 2
.= ((g || H) . I) . i by A27, A10, FUNCT_7:32
.= ((g . I) | (H . I)) . i by MSAFREE:def 1
.= (g . I) . i by Def4, FUNCT_1:49
.= (@ i) value_at (C,s) by Th61 ;
b is pure by A23;
then ( a = I implies b <> p ) by A4, Th97;
then A31: (g1 . a) . b = (((@ M),(@ i)) <- (@ x)) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s))))) by A2, A6, A23, A24, A10, AOFA_A00:def 27
.= (((@ M) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s)))))),((@ i) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s))))))) <- ((@ x) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s)))))) by Th84
.= (((@ M) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s)))))),((@ i) value_at (C,((g || H) +* (I,(supp-var p),(t value_at (C,s))))))) <- (t value_at (C,s)) by A28, Th62 ;
(g2 . a) . b = (((@ M),(@ i)) <- t) value_at (C,s) by A24, A2, A3, Th65
.= (((@ M) value_at (C,s)),((@ i) value_at (C,s))) <- (t value_at (C,s)) by Th80 ;
hence (g1 . a) . b = (g2 . a) . b by A31, A29, A30; :: thesis: verum
end;
end;
end;
thus g1 . a = g2 . a :: thesis: verum
proof
let b be Element of the generators of G . a; :: according to FUNCT_2:def 8 :: thesis: (g1 . a) . b = (g2 . a) . b
per cases ( b in (FreeGen T) . a or b nin (FreeGen T) . a ) ;
suppose b in (FreeGen T) . a ; :: thesis: (g1 . a) . b = (g2 . a) . b
hence (g1 . a) . b = (g2 . a) . b by A11; :: thesis: verum
end;
suppose b nin (FreeGen T) . a ; :: thesis: (g1 . a) . b = (g2 . a) . b
consider h1 being ManySortedFunction of T,C such that
A32: ( h1 is_homomorphism T,C & g1 = h1 || the generators of G ) by AOFA_A00:def 19;
consider h2 being ManySortedFunction of T,C such that
A33: ( h2 is_homomorphism T,C & g2 = h2 || the generators of G ) by AOFA_A00:def 19;
h1 || (FreeGen T) = h2 || (FreeGen T)
proof
let a be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: (h1 || (FreeGen T)) . a = (h2 || (FreeGen T)) . a
thus (h1 || (FreeGen T)) . a = (h2 || (FreeGen T)) . a :: thesis: verum
proof
let b be Element of (FreeGen T) . a; :: according to FUNCT_2:def 8 :: thesis: ((h1 || (FreeGen T)) . a) . b = ((h2 || (FreeGen T)) . a) . b
A34: ( H . a c= the generators of G . a & b in (FreeGen T) . a ) by PBOOLE:def 2, PBOOLE:def 18;
thus ((h1 || (FreeGen T)) . a) . b = ((h1 . a) | ((FreeGen T) . a)) . b by MSAFREE:def 1
.= (h1 . a) . b by FUNCT_1:49
.= ((h1 . a) | ( the generators of G . a)) . b by A34, FUNCT_1:49
.= (g1 . a) . b by A32, MSAFREE:def 1
.= (g2 . a) . b by A34, A11
.= ((h2 . a) | ( the generators of G . a)) . b by A33, MSAFREE:def 1
.= (h2 . a) . b by A34, FUNCT_1:49
.= ((h2 . a) | ((FreeGen T) . a)) . b by FUNCT_1:49
.= ((h2 || (FreeGen T)) . a) . b by MSAFREE:def 1 ; :: thesis: verum
end;
end;
hence (g1 . a) . b = (g2 . a) . b by A32, A33, EXTENS_1:19; :: thesis: verum
end;
end;
end;
end;
hence f . (s,(((@ M) . (@ i)) := (t,A))) = f . (s,(M := ((((@ M),(@ i)) <- t),A))) ; :: thesis: verum