let I be non empty set ; :: thesis: for H being Group-like associative multMagma-Family of I
for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
nf (s * t) = (nf s) ^ (nf t)
let H be Group-like associative multMagma-Family of I; :: thesis: for s, t being Element of (FreeProduct H) st ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 holds
nf (s * t) = (nf s) ^ (nf t)
let s, t be Element of (FreeProduct H); :: thesis: ( ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 implies nf (s * t) = (nf s) ^ (nf t) )
assume A1: ((nf s) . (len (nf s))) `1 <> ((nf t) . 1) `1 ; :: thesis: nf (s * t) = (nf s) ^ (nf t)
consider p being Element of ((FreeAtoms H) *+^+<0>) such that
A2: s = Class ((EqCl (ReductionRel H)),p) by EQREL_1:36;
consider q being Element of ((FreeAtoms H) *+^+<0>) such that
A3: t = Class ((EqCl (ReductionRel H)),q) by EQREL_1:36;
A4: the carrier of ((FreeAtoms H) *+^+<0>) = (FreeAtoms H) * by MONOID_0:61;
then reconsider p = p, q = q as FinSequence of FreeAtoms H by FINSEQ_1:def 11;
A5: s * t = Class ((EqCl (ReductionRel H)),(p ^ q)) by A2, A3, Th47;
A6: (nf s) ^ (nf t) in Class ((EqCl (ReductionRel H)),(p ^ q))
proof
A7: ( nf s is Element of ((FreeAtoms H) *+^+<0>) & nf t is Element of ((FreeAtoms H) *+^+<0>) & (nf s) ^ (nf t) is Element of ((FreeAtoms H) *+^+<0>) & p ^ q is Element of ((FreeAtoms H) *+^+<0>) ) by A4, FINSEQ_1:def 11;
[p,(nf s)] in EqCl (ReductionRel H) by A2, Def7, EQREL_1:18;
then A8: p, nf s are_convertible_wrt ReductionRel H by A7, MSUALG_6:41;
[q,(nf t)] in EqCl (ReductionRel H) by A3, Def7, EQREL_1:18;
then q, nf t are_convertible_wrt ReductionRel H by A7, MSUALG_6:41;
then p ^ q,(nf s) ^ (nf t) are_convertible_wrt ReductionRel H by A8, Th43;
then [(p ^ q),((nf s) ^ (nf t))] in EqCl (ReductionRel H) by A7, MSUALG_6:41;
hence (nf s) ^ (nf t) in Class ((EqCl (ReductionRel H)),(p ^ q)) by EQREL_1:18; :: thesis: verum
end;
A9: (nf s) ^ (nf t) is_a_normal_form_wrt ReductionRel H
proof
per cases ( t = 1_ (FreeProduct H) or t <> 1_ (FreeProduct H) ) ;
suppose A10: t <> 1_ (FreeProduct H) ; :: thesis: (nf s) ^ (nf t) is_a_normal_form_wrt ReductionRel H
assume not (nf s) ^ (nf t) is_a_normal_form_wrt ReductionRel H ; :: thesis: contradiction
then consider b being object such that
A11: [((nf s) ^ (nf t)),b] in ReductionRel H by REWRITE1:def 5;
b in rng (ReductionRel H) by A11, XTUPLE_0:def 13;
then reconsider b = b as FinSequence of FreeAtoms H by A4, FINSEQ_1:def 11;
per cases ( ex r, u being FinSequence of FreeAtoms H ex i being Element of I st
( (nf s) ^ (nf t) = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) or ex r, u being FinSequence of FreeAtoms H ex i being Element of I ex g9, h9 being Element of (H . i) st
( (nf s) ^ (nf t) = (r ^ <*[i,g9],[i,h9]*>) ^ u & b = (r ^ <*[i,(g9 * h9)]*>) ^ u ) ) by A11, Def3;
suppose ex r, u being FinSequence of FreeAtoms H ex i being Element of I st
( (nf s) ^ (nf t) = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) ; :: thesis: contradiction
then consider r, u being FinSequence of FreeAtoms H, i being Element of I such that
A12: ( (nf s) ^ (nf t) = (r ^ <*[i,(1_ (H . i))]*>) ^ u & b = r ^ u ) ;
A13: len (r ^ <*[i,(1_ (H . i))]*>) = (len r) + 1 by FINSEQ_2:16;
0 + 1 <= (len r) + 1 by XREAL_1:6;
then A14: (len r) + 1 in dom (r ^ <*[i,(1_ (H . i))]*>) by A13, FINSEQ_3:25;
then A15: (len r) + 1 in dom ((nf s) ^ (nf t)) by A12, FINSEQ_2:15;
((nf s) ^ (nf t)) . ((len r) + 1) = (r ^ <*[i,(1_ (H . i))]*>) . ((len r) + 1) by A12, A14, FINSEQ_1:def 7
.= [i,(1_ (H . i))] by FINSEQ_1:42 ;
then [i,(1_ (H . i))] in rng ((nf s) ^ (nf t)) by A15, FUNCT_1:3;
then [i,(1_ (H . i))] in (rng (nf s)) \/ (rng (nf t)) by FINSEQ_1:31;
per cases then ( [i,(1_ (H . i))] in rng (nf s) or [i,(1_ (H . i))] in rng (nf t) ) by XBOOLE_0:def 3;
suppose A16: [i,(1_ (H . i))] in rng (nf s) ; :: thesis: contradiction
then A17: nf s = (((nf s) -| [i,(1_ (H . i))]) ^ <*[i,(1_ (H . i))]*>) ^ ((nf s) |-- [i,(1_ (H . i))]) by FINSEQ_4:51;
A18: ( (nf s) -| [i,(1_ (H . i))] is FinSequence of FreeAtoms H & (nf s) |-- [i,(1_ (H . i))] is FinSequence of FreeAtoms H ) by A16, FINSEQ_4:41, FINSEQ_4:50;
then ((nf s) -| [i,(1_ (H . i))]) ^ ((nf s) |-- [i,(1_ (H . i))]) is FinSequence of FreeAtoms H by FINSEQ_1:75;
then [(nf s),(((nf s) -| [i,(1_ (H . i))]) ^ ((nf s) |-- [i,(1_ (H . i))]))] in ReductionRel H by A17, A18, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum
end;
suppose A19: [i,(1_ (H . i))] in rng (nf t) ; :: thesis: contradiction
then A20: nf t = (((nf t) -| [i,(1_ (H . i))]) ^ <*[i,(1_ (H . i))]*>) ^ ((nf t) |-- [i,(1_ (H . i))]) by FINSEQ_4:51;
A21: ( (nf t) -| [i,(1_ (H . i))] is FinSequence of FreeAtoms H & (nf t) |-- [i,(1_ (H . i))] is FinSequence of FreeAtoms H ) by A19, FINSEQ_4:41, FINSEQ_4:50;
then ((nf t) -| [i,(1_ (H . i))]) ^ ((nf t) |-- [i,(1_ (H . i))]) is FinSequence of FreeAtoms H by FINSEQ_1:75;
then [(nf t),(((nf t) -| [i,(1_ (H . i))]) ^ ((nf t) |-- [i,(1_ (H . i))]))] in ReductionRel H by A20, A21, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum
end;
end;
end;
suppose ex r, u being FinSequence of FreeAtoms H ex i being Element of I ex g9, h9 being Element of (H . i) st
( (nf s) ^ (nf t) = (r ^ <*[i,g9],[i,h9]*>) ^ u & b = (r ^ <*[i,(g9 * h9)]*>) ^ u ) ; :: thesis: contradiction
then consider r, u being FinSequence of FreeAtoms H, i being Element of I, g9, h9 being Element of (H . i) such that
A22: ( (nf s) ^ (nf t) = (r ^ <*[i,g9],[i,h9]*>) ^ u & b = (r ^ <*[i,(g9 * h9)]*>) ^ u ) ;
( (len r) + 2 <= len (nf s) or len r >= len (nf s) or (len r) + 1 = len (nf s) )
proof
assume ( not (len r) + 2 <= len (nf s) & not len r >= len (nf s) ) ; :: thesis: (len r) + 1 = len (nf s)
then ( (len (nf s)) + 1 <= ((len r) + 1) + 1 & (len r) + 1 <= len (nf s) ) by NAT_1:13;
then ( len (nf s) <= (len r) + 1 & (len r) + 1 <= len (nf s) ) by XREAL_1:6;
hence (len r) + 1 = len (nf s) by XXREAL_0:1; :: thesis: verum
end;
per cases then ( (len r) + 2 <= len (nf s) or (len r) + 1 = len (nf s) or len r >= len (nf s) ) ;
suppose (len r) + 2 <= len (nf s) ; :: thesis: contradiction
then (len r) + (len <*[i,g9],[i,h9]*>) <= len (nf s) by FINSEQ_1:44;
then len (r ^ <*[i,g9],[i,h9]*>) <= len (nf s) by FINSEQ_1:22;
then consider t9 being FinSequence such that
A23: nf s = (r ^ <*[i,g9],[i,h9]*>) ^ t9 by A22, FINSEQ_1:47;
reconsider t9 = t9 as FinSequence of FreeAtoms H by A23, FINSEQ_1:36;
set b9 = (r ^ <*[i,(g9 * h9)]*>) ^ t9;
<*[i,(g9 * h9)]*> is FinSequence of FreeAtoms H by Th23;
then (r ^ <*[i,(g9 * h9)]*>) ^ t9 is FinSequence of FreeAtoms H by FINSEQ_1:75;
then [(nf s),((r ^ <*[i,(g9 * h9)]*>) ^ t9)] in ReductionRel H by A23, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum
end;
suppose A24: (len r) + 1 = len (nf s) ; :: thesis: contradiction
(len r) + 1 <= (len r) + 2 by XREAL_1:6;
then (len r) + 1 <= (len r) + (len <*[i,g9],[i,h9]*>) by FINSEQ_1:44;
then A25: (len r) + 1 <= len (r ^ <*[i,g9],[i,h9]*>) by FINSEQ_1:22;
A26: 0 + 1 <= (len r) + 1 by XREAL_1:6;
then A27: (len r) + 1 in dom (r ^ <*[i,g9],[i,h9]*>) by A25, FINSEQ_3:25;
2 = len <*[i,g9],[i,h9]*> by FINSEQ_1:44;
then A28: 1 in dom <*[i,g9],[i,h9]*> by FINSEQ_3:25;
len (nf s) in dom (nf s) by A24, A26, FINSEQ_3:25;
then (nf s) . (len (nf s)) = ((nf s) ^ (nf t)) . (len (nf s)) by FINSEQ_1:def 7
.= (r ^ <*[i,g9],[i,h9]*>) . ((len r) + 1) by A22, A24, A27, FINSEQ_1:def 7
.= <*[i,g9],[i,h9]*> . 1 by A28, FINSEQ_1:def 7
.= [i,g9] ;
then A29: ((nf s) . (len (nf s))) `1 = i ;
A30: 0 + 1 <= (len r) + 2 by XREAL_1:7;
2 = len <*[i,g9],[i,h9]*> by FINSEQ_1:44;
then A31: 2 in dom <*[i,g9],[i,h9]*> by FINSEQ_3:25;
(len r) + 2 = (len r) + (len <*[i,g9],[i,h9]*>) by FINSEQ_1:44
.= len (r ^ <*[i,g9],[i,h9]*>) by FINSEQ_1:22 ;
then A32: (len r) + 2 in dom (r ^ <*[i,g9],[i,h9]*>) by A30, FINSEQ_3:25;
1 <= len (nf t) by A10, Th63, NAT_1:14;
then 1 in dom (nf t) by FINSEQ_3:25;
then (nf t) . 1 = ((nf s) ^ (nf t)) . ((len (nf s)) + 1) by FINSEQ_1:def 7
.= (r ^ <*[i,g9],[i,h9]*>) . ((len r) + 2) by A22, A24, A32, FINSEQ_1:def 7
.= <*[i,g9],[i,h9]*> . 2 by A31, FINSEQ_1:def 7
.= [i,h9] ;
hence contradiction by A1, A29; :: thesis: verum
end;
suppose A33: len r >= len (nf s) ; :: thesis: contradiction
(nf s) ^ (nf t) = r ^ (<*[i,g9],[i,h9]*> ^ u) by A22, FINSEQ_1:32;
then consider t9, u9 being FinSequence such that
A34: ( (nf s) ^ t9 = r & u9 ^ (<*[i,g9],[i,h9]*> ^ u) = nf t ) by A33, RFINSEQ:34;
A35: (u9 ^ <*[i,g9],[i,h9]*>) ^ u = nf t by A34, FINSEQ_1:32;
reconsider u9 = u9 as FinSequence of FreeAtoms H by A34, FINSEQ_1:36;
set b9 = (u9 ^ <*[i,(g9 * h9)]*>) ^ u;
<*[i,(g9 * h9)]*> is FinSequence of FreeAtoms H by Th23;
then (u9 ^ <*[i,(g9 * h9)]*>) ^ u is FinSequence of FreeAtoms H by FINSEQ_1:75;
then [(nf t),((u9 ^ <*[i,(g9 * h9)]*>) ^ u)] in ReductionRel H by A35, Def3;
hence contradiction by Def7, REWRITE1:def 5; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
thus nf (s * t) = (nf s) ^ (nf t) by A5, A6, A9, Def7; :: thesis: verum