let S be non empty non void ManySortedSign ; :: thesis: for s being SortSymbol of S
for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds
(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)
let s be SortSymbol of S; :: thesis: for X being V5() ManySortedSet of the carrier of S
for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds
(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)
let X be V5() ManySortedSet of the carrier of S; :: thesis: for x being Element of X . s
for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds
(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)
let x be Element of X . s; :: thesis: for t, t1 being Element of (Free (S,X)) st the_sort_of t1 = s holds
(t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)
let t, t1 be Element of (Free (S,X)); :: thesis: ( the_sort_of t1 = s implies (t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t) )
assume A: the_sort_of t1 = s ; :: thesis: (t,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of t)
defpred S1[ Element of (Free (S,X))] means ($1,[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of $1);
A0: for s1 being SortSymbol of S
for y being Element of X . s1 holds S1[y -term ]
proof
let s1 be SortSymbol of S; :: thesis: for y being Element of X . s1 holds S1[y -term ]
let y be Element of X . s1; :: thesis: S1[y -term ]
per cases ( ( s1 = s & y = x ) or [y,s1] <> [x,s] ) by XTUPLE_0:1;
suppose ( s1 = s & y = x ) ; :: thesis: S1[y -term ]
then ( ((y -term),[x,s]) <- t1 = t1 & the_sort_of (y -term) = s ) by SORT;
hence ((y -term),[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of (y -term)) by A, SORT; :: thesis: verum
end;
suppose [y,s1] <> [x,s] ; :: thesis: S1[y -term ]
then ( ((y -term),[x,s]) <- t1 = y -term & the_sort_of (y -term) = s1 ) by SORT, ThL7;
hence ((y -term),[x,s]) <- t1 in the Sorts of (Free (S,X)) . (the_sort_of (y -term)) ; :: thesis: verum
end;
end;
end;
A1: for o being OperSymbol of S
for p being Element of Args (o,(Free (S,X))) st ( for t2 being Element of (Free (S,X)) st t2 in rng p holds
S1[t2] ) 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 t2 being Element of (Free (S,X)) st t2 in rng p holds
S1[t2] ) holds
S1[o -term p]
let p be Element of Args (o,(Free (S,X))); :: thesis: ( ( for t2 being Element of (Free (S,X)) st t2 in rng p holds
S1[t2] ) implies S1[o -term p] )
assume A3: for t2 being Element of (Free (S,X)) st t2 in rng p holds
S1[t2] ; :: thesis: S1[o -term p]
per cases ( p = {} or p <> {} ) ;
suppose p = {} ; :: thesis: S1[o -term p]
then A2: o -term p = root-tree [o, the carrier of S] by TREES_4:20;
s in the carrier of S ;
then s <> the carrier of S ;
then [x,s] <> [o, the carrier of S] by XTUPLE_0:1;
then ((o -term p),[x,s]) <- t1 = o -term p by A2, ThL7;
hence S1[o -term p] by SORT; :: thesis: verum
end;
suppose A2: p <> {} ; :: thesis: S1[o -term p]
deffunc H1( Nat) -> set = ((p /. $1),[x,s]) <- t1;
consider q being FinSequence such that
A4: ( len q = len p & ( for i being Nat st i in dom q holds
q . i = H1(i) ) ) from FINSEQ_1:sch 2();
A5: ( dom q = dom p & dom p <> {} ) by A2, A4, FINSEQ_3:29;
A6: ( not p is empty & not q is empty ) by A2, A4;
A8: dom p = dom (the_arity_of o) by MSUALG_6:2;
then A9: len q = len (the_arity_of o) by A4, FINSEQ_3:29;
now :: thesis: for i being Nat st i in dom q holds
q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i)
let i be Nat; :: thesis: ( i in dom q implies q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) )
assume B1: i in dom q ; :: thesis: q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i)
then B2: p /. i = p . i by A5, PARTFUN1:def 6;
then p /. i in rng p by B1, A5, FUNCT_1:def 3;
then B3: ( S1[p /. i] & q . i = H1(i) ) by A3, A4, B1;
p . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by B1, A5, A8, MSUALG_6:2;
hence q . i in the Sorts of (Free (S,X)) . ((the_arity_of o) /. i) by B3, B2, SORT; :: thesis: verum
end;
then reconsider q = q as Element of Args (o,(Free (S,X))) by A9, MSAFREE2:5;
now :: thesis: for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,[x,s]) <- t1
let i be Nat; :: thesis: for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,[x,s]) <- t1
let d1 be DecoratedTree; :: thesis: ( i in dom p & d1 = p . i implies q . i = (d1,[x,s]) <- t1 )
assume ( i in dom p & d1 = p . i ) ; :: thesis: q . i = (d1,[x,s]) <- t1
then ( q . i = H1(i) & p /. i = d1 ) by A4, A5, PARTFUN1:def 6;
hence q . i = (d1,[x,s]) <- t1 ; :: thesis: verum
end;
then A7: ((o -term p),[x,s]) <- t1 = o -term q by A6, ThL8, A4, FINSEQ_3:29;
( the_sort_of (o -term p) = the_result_sort_of o & the_result_sort_of o = the_sort_of (o -term q) ) by Th8;
hence S1[o -term p] by A7; :: thesis: verum
end;
end;
end;
thus S1[t] from MSAFREE5:sch 2(A0, A1); :: thesis: verum