let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being non-empty 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; :: thesis: for X being non-empty 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 non-empty ManySortedSet of the carrier of S; :: thesis: 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; :: thesis: 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)); :: thesis: ( ( 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]
proof
set s0 = s;
let s be SortSymbol of S; :: thesis: for x being Element of X . s
for r being Element of (NFAlgebra R) st r = x -term holds
S1[r]
let x be Element of X . s; :: thesis: for r being Element of (NFAlgebra R) st r = x -term holds
S1[r]
let r be Element of (NFAlgebra R); :: thesis: ( r = x -term implies S1[r] )
assume Z0: r = x -term ; :: thesis: S1[r]
then A2: ( the_sort_of r = the_sort_of (@ r) & the_sort_of (@ r) = s ) by SORT, Lem00;
per cases ( ( s = s & x1 = x ) or ( s = s & x2 = x ) or s <> s or ( x1 <> x & x2 <> x ) ) ;
suppose ( s = s & x1 = x ) ; :: thesis: S1[r]
then ( ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of r)) . r = x2 -term & x2 -term = ((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r ) by Z0, A2, HOM;
hence S1[r] by ABBR; :: thesis: verum
end;
suppose ( s = s & x2 = x ) ; :: thesis: S1[r]
then ( ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of r)) . r = x1 -term & x1 -term = ((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r ) by Z0, A2, HOM;
hence S1[r] by ABBR; :: thesis: verum
end;
suppose ( s <> s or ( x1 <> x & x2 <> x ) ) ; :: thesis: S1[r]
then ( ((Hom ((Free (S,X)),x1,x2)) . (the_sort_of r)) . r = r & r = ((Hom ((NFAlgebra R),x1,x2)) . (the_sort_of r)) . r ) by Z0, A2, HOM;
hence S1[r] by ABBR; :: thesis: verum
end;
end;
end;
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; :: thesis: 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))); :: thesis: 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); :: thesis: ( 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 ; :: thesis: ( 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] ; :: thesis: 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; :: according to FINSEQ_1:def 18 :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: ((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 ; :: thesis: verum
end;
assume not S1[r] ; :: thesis: 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; :: thesis: verum
end;
hereby :: thesis: (Hom ((Free (S,X)),x1,x2)) || (NForms R) = Hom ((NFAlgebra R),x1,x2)
let t be Element of (NFAlgebra R); :: thesis: S1[t]
thus S1[t] from MSAFREE5:sch 3(A1, A2); :: thesis: verum
end;
set s0 = s;
let s be SortSymbol of S; :: according to PBOOLE:def 21 :: thesis: ((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 :: thesis: verum
proof
thus (NForms R) . s = the Sorts of (NFAlgebra R) . s by MSAFREE4:def 20; :: according to FUNCT_2:def 7 :: thesis: 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; :: thesis: (((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 ; :: thesis: verum
end;