let S be non empty non void ManySortedSign ; for X being V5() ManySortedSet of S
for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let X be V5() ManySortedSet of S; for R being invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X))
for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let R be invariant stable terminating with_UN_property ManySortedRelation of (Free (S,X)); for g being ManySortedFunction of (Free (S,X)),(Free (S,X)) st g is_homomorphism Free (S,X), Free (S,X) holds
for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let g be ManySortedFunction of (Free (S,X)),(Free (S,X)); ( g is_homomorphism Free (S,X), Free (S,X) implies for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s)) )
assume
g is_homomorphism Free (S,X), Free (S,X)
; for h being ManySortedFunction of (NFAlgebra R),(NFAlgebra R) st ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) holds
for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let h be ManySortedFunction of (NFAlgebra R),(NFAlgebra R); ( ( for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s)) ) implies for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s)) )
assume A1:
for s being SortSymbol of S
for x being Element of (NFAlgebra R),s holds (h . s) . x = nf (((g . s) . x),(R . s))
; for s being SortSymbol of S
for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let s be SortSymbol of S; for o being OperSymbol of S st s = the_result_sort_of o holds
for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let o be OperSymbol of S; ( s = the_result_sort_of o implies for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s)) )
assume A2:
s = the_result_sort_of o
; for x being Element of Args (o,(NFAlgebra R))
for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let x be Element of Args (o,(NFAlgebra R)); for y being Element of Args (o,(Free (S,X))) st x = y holds
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
let y be Element of Args (o,(Free (S,X))); ( x = y implies nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s)) )
assume A3:
x = y
; nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
defpred S1[ Nat] means ( $1 <= len (the_arity_of o) implies nf (((Den (o,(Free (S,X)))) . (((g # y) | $1) ^ ((h # x) /^ $1))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) );
( dom (h # x) = dom (the_arity_of o) & dom (g # y) = dom (the_arity_of o) )
by MSUALG_3:6;
then A4:
( len (h # x) = len (the_arity_of o) & len (g # y) = len (the_arity_of o) )
by FINSEQ_3:29;
( (g # y) | 0 = {} & (h # x) /^ 0 = h # x )
by Th81;
then A5:
((g # y) | 0) ^ ((h # x) /^ 0) = h # x
by FINSEQ_1:34;
A6:
( Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) & h # x in Args (o,(NFAlgebra R)) )
by Lm3;
then reconsider hx = h # x as Element of Args (o,(Free (S,X))) ;
( NForms R c= the Sorts of (Free (S,X)) & the Sorts of (NFAlgebra R) = NForms R )
by Def20, PBOOLE:def 18;
then
( Result (o,(Free (S,X))) = the Sorts of (Free (S,X)) . s & Result (o,(NFAlgebra R)) = the Sorts of (NFAlgebra R) . s & the Sorts of (NFAlgebra R) . s c= the Sorts of (Free (S,X)) . s & (Den (o,(NFAlgebra R))) . (h # x) in Result (o,(NFAlgebra R)) )
by A2, FUNCT_2:15;
then reconsider Dx = (Den (o,(Free (S,X)))) . hx, Dnx = (Den (o,(NFAlgebra R))) . (h # x) as Element of (Free (S,X)),s ;
nf ((nf (Dx,(R . s))),(R . s)) = nf (Dnx,(R . s))
by A2, Def20;
then A7:
S1[ 0 ]
by A5, Th18;
A8:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A9:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verumproof
assume A10:
i + 1
<= len (the_arity_of o)
;
nf (((Den (o,(Free (S,X)))) . (((g # y) | (i + 1)) ^ ((h # x) /^ (i + 1)))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s))
then A11:
i < len (the_arity_of o)
by NAT_1:13;
A12:
(
len ((h # x) | i) = i &
len ((g # y) | i) = i )
by A4, A11, FINSEQ_1:59;
A13:
(g # y) | (i + 1) = ((g # y) | i) ^ <*((g # y) . (i + 1))*>
by A4, A10, Th83;
A14:
(h # x) /^ i = <*((h # x) . (i + 1))*> ^ ((h # x) /^ (i + 1))
by A4, A10, Th84;
A15:
(
i + 1
in dom (the_arity_of o) &
dom ( the Sorts of (NFAlgebra R) * (the_arity_of o)) = dom (the_arity_of o) )
by A10, NAT_1:11, FINSEQ_3:25, PRALG_2:3;
A16:
(
x . (i + 1) in ( the Sorts of (NFAlgebra R) * (the_arity_of o)) . (i + 1) &
(the_arity_of o) /. (i + 1) = (the_arity_of o) . (i + 1) )
by A15, PARTFUN1:def 6, MSUALG_3:6;
then reconsider xi1 =
x . (i + 1) as
Element of
(NFAlgebra R),
((the_arity_of o) /. (i + 1)) by A15, FUNCT_1:13;
dom x = dom (the_arity_of o)
by MSUALG_3:6;
then (h # x) . (i + 1) =
(h . ((the_arity_of o) /. (i + 1))) . xi1
by A15, MSUALG_3:def 6
.=
nf (
((g . ((the_arity_of o) /. (i + 1))) . xi1),
(R . ((the_arity_of o) /. (i + 1))))
by A1
;
then
hx . (i + 1) is_a_normal_form_of (g . ((the_arity_of o) /. (i + 1))) . xi1,
R . ((the_arity_of o) /. (i + 1))
by REWRITE1:54;
then A17:
R . ((the_arity_of o) /. (i + 1)) reduces (g . ((the_arity_of o) /. (i + 1))) . xi1,
hx . (i + 1)
;
A18:
dom (h # x) = dom (the_arity_of o)
by MSUALG_3:6;
then A19:
len (h # x) = len (the_arity_of o)
by FINSEQ_3:29;
defpred S2[
set ]
means nf (
((Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*$1*>) ^ ((h # x) /^ (i + 1)))),
(R . s))
= nf (
((Den (o,(NFAlgebra R))) . (h # x)),
(R . s));
A20:
S2[
hx . (i + 1)]
by A9, A10, NAT_1:13, A14, FINSEQ_1:32;
A21:
for
a,
b being
set st
[a,b] in R . ((the_arity_of o) /. (i + 1)) &
S2[
b] holds
S2[
a]
proof
let a,
b be
set ;
( [a,b] in R . ((the_arity_of o) /. (i + 1)) & S2[b] implies S2[a] )
assume A22:
[a,b] in R . ((the_arity_of o) /. (i + 1))
;
( not S2[b] or S2[a] )
then reconsider c =
a,
d =
b as
Element of the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. (i + 1)) by ZFMISC_1:87;
reconsider j =
i + 1 as
Element of
NAT by ORDINAL1:def 12;
set f =
transl (
o,
j,
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),
(Free (S,X)));
now ( dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o) & dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) & ( for a being object st a in dom (the_arity_of o) holds
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a ) )A23:
len (((g # y) | i) ^ <*d*>) =
i + (len <*d*>)
by A12, FINSEQ_1:22
.=
i + 1
by FINSEQ_1:40
;
thus A24:
dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom (the_arity_of o)
by PRALG_2:3;
( dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) & ( for a being object st a in dom (the_arity_of o) holds
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b2 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b2 ) ) len ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) =
(len (((g # y) | i) ^ <*d*>)) + (len ((h # x) /^ (i + 1)))
by FINSEQ_1:22
.=
(i + 1) + ((len (h # x)) - (i + 1))
by A10, A19, A23, RFINSEQ:def 1
.=
len (the_arity_of o)
by A18, FINSEQ_3:29
;
hence
dom ( the Sorts of (Free (S,X)) * (the_arity_of o)) = dom ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)))
by A24, FINSEQ_3:29;
for a being object st a in dom (the_arity_of o) holds
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b2 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b2let a be
object ;
( a in dom (the_arity_of o) implies ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b1 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b1 )assume A25:
a in dom (the_arity_of o)
;
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b1 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b1then reconsider b =
a as
Nat ;
A26:
(
b <= len (the_arity_of o) &
b >= 1 )
by A25, FINSEQ_3:25;
per cases
( b <= i or b = i + 1 or b > i + 1 )
by NAT_1:8;
suppose A27:
b <= i
;
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b1 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b1then A28:
(
b in dom ((g # y) | i) &
dom ((g # y) | i) c= dom (((g # y) | i) ^ <*d*>) &
b in Seg i )
by A26, A12, FINSEQ_3:25, FINSEQ_1:26;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a =
(((g # y) | i) ^ <*d*>) . a
by FINSEQ_1:def 7
.=
((g # y) | i) . a
by A28, FINSEQ_1:def 7
.=
(g # y) . a
by A27, A26, FINSEQ_1:1, FUNCT_1:49
;
hence
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a
by A24, A25, MSUALG_3:6;
verum end; suppose A30:
b > i + 1
;
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . b1 in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . b1then consider k being
Nat such that A31:
b = (i + 1) + k
by NAT_1:10;
(i + 1) + k > (i + 1) + 0
by A30, A31;
then
(
k > 0 &
b - (i + 1) <= (len (the_arity_of o)) - (i + 1) )
by A26, XREAL_1:9, XREAL_1:6;
then
(
k >= 0 + 1 &
k <= len ((h # x) /^ (i + 1)) )
by A10, A19, RFINSEQ:def 1, A31, NAT_1:13;
then A32:
k in dom ((h # x) /^ (i + 1))
by FINSEQ_3:25;
then ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a =
((h # x) /^ (i + 1)) . k
by A23, A31, FINSEQ_1:def 7
.=
(h # x) . a
by A31, A19, A32, A10, RFINSEQ:def 1
;
hence
((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) . a in ( the Sorts of (Free (S,X)) * (the_arity_of o)) . a
by A24, A25, A6, MSUALG_3:6;
verum end; end; end;
then A33:
(((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) in product ( the Sorts of (Free (S,X)) * (the_arity_of o))
by CARD_3:9;
then
(((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) in Args (
o,
(Free (S,X)))
by PRALG_2:3;
then A34:
[((transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . c),((transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . d)] in R . s
by A2, A15, A22, MSUALG_6:def 5, MSUALG_6:def 8;
reconsider ad =
(((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)) as
Element of
Args (
o,
(Free (S,X)))
by A33, PRALG_2:3;
reconsider Dd =
(Den (o,(Free (S,X)))) . ad as
Element of
(Free (S,X)),
s by A2, FUNCT_2:15;
A35:
(transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . c =
(Den (o,(Free (S,X)))) . (((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) +* (j,c))
by MSUALG_6:def 4
.=
(Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*c*>) ^ ((h # x) /^ (i + 1)))
by A12, Th82
;
(transl (o,j,((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))),(Free (S,X)))) . d =
(Den (o,(Free (S,X)))) . (((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) +* (j,d))
by MSUALG_6:def 4
.=
(Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1)))
by A12, Th82
;
then A36:
(Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*c*>) ^ ((h # x) /^ (i + 1))),
(Den (o,(Free (S,X)))) . ((((g # y) | i) ^ <*d*>) ^ ((h # x) /^ (i + 1))) are_convertible_wrt R . s
by A34, A35, REWRITE1:29;
assume
S2[
b]
;
S2[a]
hence
S2[
a]
by A36, REWRITE1:55;
verum
end;
A37:
S2[
(g . ((the_arity_of o) /. (i + 1))) . xi1]
from MSAFREE4:sch 6(A20, A17, A21);
dom y = dom (the_arity_of o)
by MSUALG_3:6;
hence
nf (
((Den (o,(Free (S,X)))) . (((g # y) | (i + 1)) ^ ((h # x) /^ (i + 1)))),
(R . s))
= nf (
((Den (o,(NFAlgebra R))) . (h # x)),
(R . s))
by A13, A3, A15, A37, MSUALG_3:def 6;
verum
end; end;
for i being Nat holds S1[i]
from NAT_1:sch 2(A7, A8);
then A38:
nf (((Den (o,(Free (S,X)))) . (((g # y) | (len (the_arity_of o))) ^ ((h # x) /^ (len (the_arity_of o))))),(R . s)) = nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s))
;
( (g # y) | (len (the_arity_of o)) = g # y & (h # x) /^ (len (the_arity_of o)) = {} )
by A4, FINSEQ_1:58, Th81;
hence
nf (((Den (o,(NFAlgebra R))) . (h # x)),(R . s)) = nf (((Den (o,(Free (S,X)))) . (g # y)),(R . s))
by A38, FINSEQ_1:34; verum