let S be non empty non void ManySortedSign ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for R being invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X))
for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t
let R be invariant stable terminating with_UN_property NF-var ManySortedRelation of (Free (S,X)); :: thesis: for t being Element of (Free (S,X)) holds R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t
let t be Element of (Free (S,X)); :: thesis: R . (the_sort_of t) reduces t,(canonical_homomorphism (NFAlgebra R)) . t
set T = NFAlgebra R;
set H = canonical_homomorphism (NFAlgebra R);
defpred S1[ Element of (Free (S,X))] means R . (the_sort_of $1) reduces $1,(canonical_homomorphism (NFAlgebra R)) . $1;
A1: for s being SortSymbol of S
for x being Element of X . s holds S1[x -term ] by REWRITE1:12;
A2: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
proof
let o be OperSymbol of S; :: thesis: for p being Element of Args (o,(Free (S,X))) st ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) holds
S1[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ) implies S1[o -term p] )
assume Z0: for t being Element of (Free (S,X)) st t in rng p holds
S1[t] ; :: thesis: S1[o -term p]
A3: o -term p = (Den (o,(Free (S,X)))) . p by MSAFREE4:13;
A4: the_sort_of (o -term p) = the_result_sort_of o by Th8;
then (canonical_homomorphism (NFAlgebra R)) . (o -term p) = ((canonical_homomorphism (NFAlgebra R)) . (the_result_sort_of o)) . (o -term p) by ABBR
.= (Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) by A3, MSUALG_3:def 7, MSAFREE4:def 10
.= nf (((Den (o,(Free (S,X)))) . ((canonical_homomorphism (NFAlgebra R)) # p)),(R . (the_result_sort_of o))) by MSAFREE4:def 20 ;
then A5: (canonical_homomorphism (NFAlgebra R)) . (o -term p) is_a_normal_form_of (Den (o,(Free (S,X)))) . ((canonical_homomorphism (NFAlgebra R)) # p),R . (the_result_sort_of o) by REWRITE1:54;
per cases ( len p = 0 or len p <> 0 ) ;
suppose len p = 0 ; :: thesis: S1[o -term p]
then ( dom p = Seg 0 & Seg 0 = {} ) by FINSEQ_1:def 3;
then ( dom ((canonical_homomorphism (NFAlgebra R)) # p) = dom (the_arity_of o) & dom (the_arity_of o) = {} & {} = dom p ) by MSUALG_6:2;
then ( (canonical_homomorphism (NFAlgebra R)) # p = {} & {} = p ) ;
then ( o -term p = (Den (o,(Free (S,X)))) . ((canonical_homomorphism (NFAlgebra R)) # p) & nf (((Den (o,(Free (S,X)))) . ((canonical_homomorphism (NFAlgebra R)) # p)),(R . (the_result_sort_of o))) = (Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) & (Den (o,(NFAlgebra R))) . ((canonical_homomorphism (NFAlgebra R)) # p) = ((canonical_homomorphism (NFAlgebra R)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p) ) by MSUALG_3:def 7, MSAFREE4:13, MSAFREE4:def 20, MSAFREE4:def 10;
then A6: ((canonical_homomorphism (NFAlgebra R)) . (the_result_sort_of o)) . ((Den (o,(Free (S,X)))) . p) is_a_normal_form_of o -term p,R . (the_result_sort_of o) by REWRITE1:54;
the_sort_of (o -term p) = the_result_sort_of o by Th8;
hence S1[o -term p] by A3, A6, ABBR; :: thesis: verum
end;
suppose B0: len p <> 0 ; :: thesis: S1[o -term p]
deffunc H1( FinSequence, Nat) -> set = $1 +* ($2,(((canonical_homomorphism (NFAlgebra R)) # p) . $2));
defpred S2[ Nat, set , set ] means ex r being FinSequence st
( $2 = r & $3 = H1(r,$1 + 1) );
A7: for r being Element of Args (o,(Free (S,X)))
for n being Nat st 1 <= n & n <= len p holds
H1(r,n) in Args (o,(Free (S,X)))
proof
Args (o,(NFAlgebra R)) c= Args (o,(Free (S,X))) by MSAFREE4:41;
then C1: (canonical_homomorphism (NFAlgebra R)) # p in Args (o,(Free (S,X))) ;
let r be Element of Args (o,(Free (S,X))); :: thesis: for n being Nat st 1 <= n & n <= len p holds
H1(r,n) in Args (o,(Free (S,X)))
let n be Nat; :: thesis: ( 1 <= n & n <= len p implies H1(r,n) in Args (o,(Free (S,X))) )
assume ( 1 <= n & n <= len p ) ; :: thesis: H1(r,n) in Args (o,(Free (S,X)))
then ( n in dom p & dom p = dom (the_arity_of o) ) by MSUALG_3:6, FINSEQ_3:25;
then ((canonical_homomorphism (NFAlgebra R)) # p) . n in the Sorts of (Free (S,X)) . ((the_arity_of o) /. n) by C1, MSUALG_6:2;
hence H1(r,n) in Args (o,(Free (S,X))) by MSUALG_6:7; :: thesis: verum
end;
A6: for n being Nat st 1 <= n & n < len p holds
for x being Element of Args (o,(Free (S,X))) ex y being Element of Args (o,(Free (S,X))) st S2[n,x,y]
proof
let n be Nat; :: thesis: ( 1 <= n & n < len p implies for x being Element of Args (o,(Free (S,X))) ex y being Element of Args (o,(Free (S,X))) st S2[n,x,y] )
assume 1 <= n ; :: thesis: ( not n < len p or for x being Element of Args (o,(Free (S,X))) ex y being Element of Args (o,(Free (S,X))) st S2[n,x,y] )
assume Z1: n < len p ; :: thesis: for x being Element of Args (o,(Free (S,X))) ex y being Element of Args (o,(Free (S,X))) st S2[n,x,y]
let x be Element of Args (o,(Free (S,X))); :: thesis: ex y being Element of Args (o,(Free (S,X))) st S2[n,x,y]
( 1 <= n + 1 & n + 1 <= len p ) by Z1, NAT_1:12, NAT_1:13;
then reconsider y = H1(x,n + 1) as Element of Args (o,(Free (S,X))) by A7;
take y ; :: thesis: S2[n,x,y]
thus S2[n,x,y] ; :: thesis: verum
end;
B2: len p >= 0 + 1 by B0, NAT_1:13;
reconsider f1 = H1(p,1) as Element of Args (o,(Free (S,X))) by A7, B2;
consider f being FinSequence of Args (o,(Free (S,X))) such that
B3: ( len f = len p & ( f . 1 = f1 or len p = 0 ) & ( for n being Nat st 1 <= n & n < len p holds
S2[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 4(A6);
B6: dom f = dom p by B3, FINSEQ_3:29;
defpred S3[ Nat] means ( $1 <= len p implies ( dom (f . $1) = dom p & ( for i being Nat st 1 <= i & i <= $1 holds
(f . $1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i ) & ( for i being Nat st $1 + 1 <= i & i <= len p holds
(f . $1) . i = p . i ) ) );
BA: S3[1]
proof
assume 1 <= len p ; :: thesis: ( dom (f . 1) = dom p & ( for i being Nat st 1 <= i & i <= 1 holds
(f . 1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i ) & ( for i being Nat st 1 + 1 <= i & i <= len p holds
(f . 1) . i = p . i ) )
then C0: 1 in dom p by FINSEQ_3:25;
thus dom (f . 1) = dom p by B0, B3, FUNCT_7:30; :: thesis: ( ( for i being Nat st 1 <= i & i <= 1 holds
(f . 1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i ) & ( for i being Nat st 1 + 1 <= i & i <= len p holds
(f . 1) . i = p . i ) )
hereby :: thesis: for i being Nat st 1 + 1 <= i & i <= len p holds
(f . 1) . i = p . i
let i be Nat; :: thesis: ( 1 <= i & i <= 1 implies (f . 1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i )
assume ( 1 <= i & i <= 1 ) ; :: thesis: (f . 1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i
then i = 1 by XXREAL_0:1;
hence (f . 1) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i by B0, B3, C0, FUNCT_7:31; :: thesis: verum
end;
let i be Nat; :: thesis: ( 1 + 1 <= i & i <= len p implies (f . 1) . i = p . i )
assume C1: ( 1 + 1 <= i & i <= len p ) ; :: thesis: (f . 1) . i = p . i
i > 1 by C1, NAT_1:13;
hence (f . 1) . i = p . i by B0, B3, FUNCT_7:32; :: thesis: verum
end;
BB: for j being Nat st j >= 1 & S3[j] holds
S3[j + 1]
proof
let j be Nat; :: thesis: ( j >= 1 & S3[j] implies S3[j + 1] )
assume that
D1: ( j >= 1 & S3[j] ) and
D2: j + 1 <= len p ; :: thesis: ( dom (f . (j + 1)) = dom p & ( for i being Nat st 1 <= i & i <= j + 1 holds
(f . (j + 1)) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i ) & ( for i being Nat st (j + 1) + 1 <= i & i <= len p holds
(f . (j + 1)) . i = p . i ) )
D7: ( j + 1 >= 1 & j <= j + 1 ) by NAT_1:12;
consider r being FinSequence such that
D4: ( f . j = r & f . (j + 1) = H1(r,j + 1) ) by D1, B3, D2, NAT_1:13;
thus dom (f . (j + 1)) = dom p by D1, D7, D4, D2, XXREAL_0:2, FUNCT_7:30; :: thesis: ( ( for i being Nat st 1 <= i & i <= j + 1 holds
(f . (j + 1)) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i ) & ( for i being Nat st (j + 1) + 1 <= i & i <= len p holds
(f . (j + 1)) . i = p . i ) )
hereby :: thesis: for i being Nat st (j + 1) + 1 <= i & i <= len p holds
(f . (j + 1)) . i = p . i
let i be Nat; :: thesis: ( 1 <= i & i <= j + 1 implies (f . (j + 1)) . b1 = ((canonical_homomorphism (NFAlgebra R)) # p) . b1 )
assume D6: ( 1 <= i & i <= j + 1 ) ; :: thesis: (f . (j + 1)) . b1 = ((canonical_homomorphism (NFAlgebra R)) # p) . b1
per cases ( i <= j or i >= j + 1 ) by NAT_1:13;
suppose i <= j ; :: thesis: (f . (j + 1)) . b1 = ((canonical_homomorphism (NFAlgebra R)) # p) . b1
then ( (f . j) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i & i < j + 1 ) by D1, D2, D6, NAT_1:13;
hence (f . (j + 1)) . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i by D4, FUNCT_7:32; :: thesis: verum
end;
end;
end;
let i be Nat; :: thesis: ( (j + 1) + 1 <= i & i <= len p implies (f . (j + 1)) . i = p . i )
assume D8: ( (j + 1) + 1 <= i & i <= len p ) ; :: thesis: (f . (j + 1)) . i = p . i
D10: j + 1 < i by D8, NAT_1:13;
then (f . j) . i = p . i by D1, D2, D7, D8, XXREAL_0:2;
hence (f . (j + 1)) . i = p . i by D4, D10, FUNCT_7:32; :: thesis: verum
end;
BC: for j being Nat st j >= 1 holds
S3[j] from NAT_1:sch 8(BA, BB);
defpred S4[ Nat] means ( $1 <= len p implies R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . (f . $1) );
B4: S4[1]
proof
assume 1 <= len p ; :: thesis: R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . (f . 1)
then C0: ( 1 in dom p & dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom ((canonical_homomorphism (NFAlgebra R)) # p) ) by FINSEQ_3:25, MSUALG_6:2;
then C1: ( p /. 1 = p . 1 & p . 1 in rng p ) by PARTFUN1:def 6, FUNCT_1:def 3;
then S1[p /. 1] by Z0;
then C2: R . (the_sort_of (p /. 1)) reduces p /. 1,((canonical_homomorphism (NFAlgebra R)) . (the_sort_of (p /. 1))) . (p /. 1) by ABBR;
reconsider t = ((canonical_homomorphism (NFAlgebra R)) # p) /. 1 as Element of (Free (S,X)) by MSAFREE4:39;
C3: the_sort_of (p /. 1) = (the_arity_of o) /. 1 by C0, Th4A;
then ( ((canonical_homomorphism (NFAlgebra R)) . (the_sort_of (p /. 1))) . (p /. 1) = ((canonical_homomorphism (NFAlgebra R)) # p) . 1 & ((canonical_homomorphism (NFAlgebra R)) # p) . 1 = t & p +* (1,(p /. 1)) = p ) by C0, C1, PARTFUN1:def 6, FUNCT_7:35, MSUALG_3:def 6;
hence R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . (f . 1) by A3, B0, B3, C0, C2, C3, Th113; :: thesis: verum
end;
B5: for i being Nat st i >= 1 & S4[i] holds
S4[i + 1]
proof
let i be Nat; :: thesis: ( i >= 1 & S4[i] implies S4[i + 1] )
assume D1: ( i >= 1 & S4[i] & i + 1 <= len p ) ; :: thesis: R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . (f . (i + 1))
then D2: ( i < len p & 1 <= i + 1 ) by NAT_1:13;
then C0: ( i in dom p & i + 1 in dom p & dom p = dom (the_arity_of o) & dom (the_arity_of o) = dom ((canonical_homomorphism (NFAlgebra R)) # p) ) by D1, FINSEQ_3:25, MSUALG_6:2;
then C1: ( p /. (i + 1) = p . (i + 1) & p . (i + 1) in rng p ) by PARTFUN1:def 6, FUNCT_1:def 3;
then S1[p /. (i + 1)] by Z0;
then C2: R . (the_sort_of (p /. (i + 1))) reduces p /. (i + 1),((canonical_homomorphism (NFAlgebra R)) . (the_sort_of (p /. (i + 1)))) . (p /. (i + 1)) by ABBR;
reconsider t = ((canonical_homomorphism (NFAlgebra R)) # p) /. (i + 1) as Element of (Free (S,X)) by MSAFREE4:39;
reconsider fi = f . i, fi1 = f . (i + 1) as Element of Args (o,(Free (S,X))) by B6, D2, D1, FINSEQ_3:25, FUNCT_1:102;
D3: ( fi . (i + 1) = p . (i + 1) & dom fi = dom (the_arity_of o) ) by BC, D1, D2, MSUALG_6:2;
C3: the_sort_of (p /. (i + 1)) = (the_arity_of o) /. (i + 1) by C0, Th4A;
then C4: ( ((canonical_homomorphism (NFAlgebra R)) . (the_sort_of (p /. (i + 1)))) . (p /. (i + 1)) = ((canonical_homomorphism (NFAlgebra R)) # p) . (i + 1) & ((canonical_homomorphism (NFAlgebra R)) # p) . (i + 1) = t & fi +* ((i + 1),(p /. (i + 1))) = fi ) by D3, C0, C1, PARTFUN1:def 6, FUNCT_7:35, MSUALG_3:def 6;
then C5: R . (the_result_sort_of o) reduces (Den (o,(Free (S,X)))) . fi,(Den (o,(Free (S,X)))) . (fi +* ((i + 1),t)) by D3, C0, C2, C3, Th113;
consider r being FinSequence such that
C6: ( fi = r & fi1 = H1(r,i + 1) ) by B3, D1, NAT_1:13;
thus R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . (f . (i + 1)) by C4, C5, C6, D1, NAT_1:13, REWRITE1:16; :: thesis: verum
end;
BD: for i being Nat st i >= 1 holds
S4[i] from NAT_1:sch 8(B4, B5);
reconsider fl = f . (len p) as Element of Args (o,(Free (S,X))) by B6, FUNCT_1:102, B2, FINSEQ_3:25;
fl = (canonical_homomorphism (NFAlgebra R)) # p
proof
E1: ( dom fl = dom (the_arity_of o) & dom (the_arity_of o) = dom ((canonical_homomorphism (NFAlgebra R)) # p) & dom (the_arity_of o) = dom p ) by MSUALG_6:2;
hence len fl = len ((canonical_homomorphism (NFAlgebra R)) # p) by FINSEQ_3:29; :: according to FINSEQ_1:def 18 :: thesis: for b1 being set holds
( not 1 <= b1 or not b1 <= len fl or fl . b1 = ((canonical_homomorphism (NFAlgebra R)) # p) . b1 )
E2: len fl = len p by E1, FINSEQ_3:29;
let i be Nat; :: thesis: ( not 1 <= i or not i <= len fl or fl . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i )
assume ( 1 <= i & i <= len fl ) ; :: thesis: fl . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i
hence fl . i = ((canonical_homomorphism (NFAlgebra R)) # p) . i by BC, B2, E2; :: thesis: verum
end;
then R . (the_result_sort_of o) reduces o -term p,(Den (o,(Free (S,X)))) . ((canonical_homomorphism (NFAlgebra R)) # p) by B2, BD;
hence S1[o -term p] by A4, A5, REWRITE1:16; :: thesis: verum
end;
end;
end;
thus S1[t] from MSAFREE5:sch 2(A1, A2); :: thesis: verum