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 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; 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; 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; 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)); ( 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
; (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 ]
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;
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)));
( ( 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]
;
S1[o -term p]
per cases
( p = {} or p <> {} )
;
suppose A2:
p <> {}
;
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 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;
( 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
;
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;
verum end; then reconsider q =
q as
Element of
Args (
o,
(Free (S,X)))
by A9, MSAFREE2:5;
now for i being Nat
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,[x,s]) <- t1let i be
Nat;
for d1 being DecoratedTree st i in dom p & d1 = p . i holds
q . i = (d1,[x,s]) <- t1let d1 be
DecoratedTree;
( i in dom p & d1 = p . i implies q . i = (d1,[x,s]) <- t1 )assume
(
i in dom p &
d1 = p . i )
;
q . i = (d1,[x,s]) <- t1then
(
q . i = H1(
i) &
p /. i = d1 )
by A4, A5, PARTFUN1:def 6;
hence
q . i = (
d1,
[x,s])
<- t1
;
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;
verum end; end;
end;
thus
S1[t]
from MSAFREE5:sch 2(A0, A1); verum