let S be non empty non void ManySortedSign ; for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds
( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )
let s be SortSymbol of S; for X being V5() ManySortedSet of the carrier of S
for x1, x2 being Element of X . s
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds
( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )
let X be V5() ManySortedSet of the carrier of S; for x1, x2 being Element of X . s
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds
( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )
let x1, x2 be Element of X . s; for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)) holds
( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)); ( ( for t being Element of (NFAlgebra R) holds ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = (Hom ((NFAlgebra R),x1,x2)) . t ) & (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2) )
set F = Free (S,X);
set T = NFAlgebra R;
set HF = Hom ((Free (S,X)),x1,x2);
set HN = Hom ((NFAlgebra R),x1,x2);
set N = NForms R;
defpred S1[ Element of (NFAlgebra R)] means ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of $1)) . $1 = (Hom ((NFAlgebra R),x1,x2)) . $1;
A1:
for s being SortSymbol of S
for x being Element of X . s
for r being Element of (NFAlgebra R) st r = x -term holds
S1[r]
A2:
for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X)))
for r being Element of (NFAlgebra R) st r = o -term p & ( for t being Element of (NFAlgebra R) st t in rng p holds
S1[t] ) holds
S1[r]
proof
let o be
OperSymbol of
S;
for p being Element of Args (o,(Free (S,X)))
for r being Element of (NFAlgebra R) st r = o -term p & ( for t being Element of (NFAlgebra R) st t in rng p holds
S1[t] ) holds
S1[r]let p be
Element of
Args (
o,
(Free (S,X)));
for r being Element of (NFAlgebra R) st r = o -term p & ( for t being Element of (NFAlgebra R) st t in rng p holds
S1[t] ) holds
S1[r]let r be
Element of
(NFAlgebra R);
( r = o -term p & ( for t being Element of (NFAlgebra R) st t in rng p holds
S1[t] ) implies S1[r] )
assume Z1:
r = o -term p
;
( ex t being Element of (NFAlgebra R) st
( t in rng p & not S1[t] ) or S1[r] )
then A3:
(
the_sort_of r = the_sort_of (@ r) &
the_sort_of (@ r) = the_result_sort_of o )
by Lem00, Th8;
assume Z2:
for
t being
Element of
(NFAlgebra R) st
t in rng p holds
S1[
t]
;
S1[r]
A4:
(
Hom (
(Free (S,X)),
x1,
x2)
is_homomorphism Free (
S,
X),
Free (
S,
X) &
o -term p = (Den (o,(Free (S,X)))) . p )
by MSUALG_6:def 2, MSAFREE4:13;
then A6:
((Hom ((Free (S,X)),x1,x2)) . (the_sort_of r)) . r = (Den (o,(Free (S,X)))) . ((Hom ((Free (S,X)),x1,x2)) # p)
by Z1, A3, MSUALG_3:def 7;
A7:
r in the
Sorts of
(NFAlgebra R) . (the_result_sort_of o)
by A3, SORT;
then A5:
(
p in Args (
o,
(NFAlgebra R)) &
(Den (o,(NFAlgebra R))) . p = o -term p )
by A4, Z1, MSAFREE4:def 8;
reconsider q =
p as
Element of
Args (
o,
(NFAlgebra R))
by A7, A4, Z1, MSAFREE4:def 8;
(
((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r = (Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # q) &
(Den (o,(NFAlgebra R))) . ((Hom ((NFAlgebra R),x1,x2)) # q) = nf (
((Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # q)),
(R . (the_result_sort_of o))) )
by Z1, A3, A5, MSUALG_3:def 7, MSAFREE4:def 20, MSUALG_6:def 2;
then
((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r is_a_normal_form_of (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # q),
R . (the_result_sort_of o)
by REWRITE1:54;
then
R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # q),
((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r
;
then consider m being
RedSequence of
R . (the_result_sort_of o) such that C1:
(
m . 1
= (Den (o,(Free (S,X)))) . ((Hom ((NFAlgebra R),x1,x2)) # q) &
m . (len m) = ((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r )
;
C2:
(Hom ((Free (S,X)),x1,x2)) # p = (Hom ((NFAlgebra R),x1,x2)) # q
proof
B1:
(
dom ((Hom ((Free (S,X)),x1,x2)) # p) = dom (the_arity_of o) &
dom (the_arity_of o) = dom ((Hom ((NFAlgebra R),x1,x2)) # q) &
dom p = dom (the_arity_of o) &
dom (the_arity_of o) = dom q )
by MSUALG_3:6;
hence
len ((Hom ((Free (S,X)),x1,x2)) # p) = len ((Hom ((NFAlgebra R),x1,x2)) # q)
by FINSEQ_3:29;
FINSEQ_1:def 17 for b1 being set holds
( not 1 <= b1 or not b1 <= len ((Hom ((Free (S,X)),x1,x2)) # p) or ((Hom ((Free (S,X)),x1,x2)) # p) . b1 = ((Hom ((NFAlgebra R),x1,x2)) # q) . b1 )
let i be
Nat;
( not 1 <= i or not i <= len ((Hom ((Free (S,X)),x1,x2)) # p) or ((Hom ((Free (S,X)),x1,x2)) # p) . i = ((Hom ((NFAlgebra R),x1,x2)) # q) . i )
assume B0:
( 1
<= i &
i <= len ((Hom ((Free (S,X)),x1,x2)) # p) )
;
((Hom ((Free (S,X)),x1,x2)) # p) . i = ((Hom ((NFAlgebra R),x1,x2)) # q) . i
then
i in dom ((Hom ((Free (S,X)),x1,x2)) # p)
by FINSEQ_3:25;
then B3:
(
p . i in rng p &
q . i in rng q )
by B1, FUNCT_1:def 3;
then reconsider t =
q . i as
Element of
(NFAlgebra R) by RELAT_1:167;
A8:
(
p . i = p /. i &
q . i = q /. i )
by B1, B0, FINSEQ_3:25, PARTFUN1:def 6;
then
(
p /. i in the
Sorts of
(Free (S,X)) . ((the_arity_of o) /. i) &
q /. i in the
Sorts of
(NFAlgebra R) . ((the_arity_of o) /. i) )
by B1, B0, FINSEQ_3:25, MSUALG_6:2;
then A7:
(
the_sort_of (p /. i) = (the_arity_of o) /. i &
(the_arity_of o) /. i = the_sort_of (q /. i) )
by SORT;
thus ((Hom ((Free (S,X)),x1,x2)) # p) . i =
((Hom ((Free (S,X)),x1,x2)) . ((the_arity_of o) /. i)) . (p /. i)
by B1, B0, A8, FINSEQ_3:25, MSUALG_3:def 6
.=
(Hom ((NFAlgebra R),x1,x2)) . t
by Z2, B3, A7, A8
.=
((Hom ((NFAlgebra R),x1,x2)) . ((the_arity_of o) /. i)) . (q . i)
by A7, A8, ABBR
.=
((Hom ((NFAlgebra R),x1,x2)) # q) . i
by B1, B0, FINSEQ_3:25, MSUALG_3:def 6
;
verum
end;
assume
not
S1[
r]
;
contradiction
then AA:
(
len m <> 1 &
len m >= 0 + 1 )
by C1, C2, A6, ABBR, NAT_1:13;
then
len m > 1
by XXREAL_0:1;
then
len m >= 1
+ 1
by NAT_1:13;
then
( 1
in dom m & 1
+ 1
in dom m )
by AA, FINSEQ_3:25;
then
[(m . 1),(m . 2)] in R . (the_result_sort_of o)
by REWRITE1:def 2;
then AB:
[(((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (m . 1)),(((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (m . 2))] in R . (the_result_sort_of o)
by MSUALG_6:def 9;
((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (m . 1) =
(((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) * ((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o))) . ((Den (o,(Free (S,X)))) . p)
by A3, A4, A6, Z1, C1, C2, FUNCT_2:15
.=
(((Hom ((Free (S,X)),x1,x2)) ** (Hom ((Free (S,X)),x1,x2))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p)
by MSUALG_3:2
.=
((id the Sorts of (Free (S,X))) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p)
by Th157
.=
(id ( the Sorts of (Free (S,X)) . (the_result_sort_of o))) . (o -term p)
by A4, MSUALG_3:def 1
.=
nf (
((Den (o,(Free (S,X)))) . q),
(R . (the_result_sort_of o)))
by A5, MSAFREE4:def 20
;
then
((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (m . 1) is_a_normal_form_of (Den (o,(Free (S,X)))) . q,
R . (the_result_sort_of o)
by REWRITE1:54;
then
((Hom ((Free (S,X)),x1,x2)) . (the_result_sort_of o)) . (m . 1) is_a_normal_form_wrt R . (the_result_sort_of o)
;
hence
contradiction
by AB;
verum
end;
set s0 = s;
let s be SortSymbol of S; PBOOLE:def 21 ((Hom ((Free (S,X)),x1,x2)) || (NForms R)) . s = (Hom ((NFAlgebra R),x1,x2)) . s
thus
((Hom ((Free (S,X)),x1,x2)) || (NForms R)) . s = (Hom ((NFAlgebra R),x1,x2)) . s
verumproof
thus
(NForms R) . s = the
Sorts of
(NFAlgebra R) . s
by MSAFREE4:def 20;
FUNCT_2:def 7 for b1 being Element of (NForms R) . s holds (((Hom ((Free (S,X)),x1,x2)) || (NForms R)) . s) . b1 = ((Hom ((NFAlgebra R),x1,x2)) . s) . b1
let a be
Element of
(NForms R) . s;
(((Hom ((Free (S,X)),x1,x2)) || (NForms R)) . s) . a = ((Hom ((NFAlgebra R),x1,x2)) . s) . a
reconsider t =
a as
Element of
(NFAlgebra R),
s by MSAFREE4:def 20;
S1[
t]
from MSAFREE5:sch 3(A1, A2);
then AD:
((Hom ((Free (S,X)),x1,x2)) . (the_sort_of t)) . t = ((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of t)) . t
by ABBR;
AE:
the_sort_of t = s
by SORT;
thus (((Hom ((Free (S,X)),x1,x2)) || (NForms R)) . s) . a =
(((Hom ((Free (S,X)),x1,x2)) . s) | ((NForms R) . s)) . a
by MSAFREE:def 1
.=
((Hom ((NFAlgebra R),x1,x2)) . s) . a
by AD, AE, FUNCT_1:49
;
verum
end;