let S be non empty non void ManySortedSign ; for X being non-empty ManySortedSet of S
for A2 being b1,S -terms all_vars_including inheriting_operations MSAlgebra over S
for t being Element of A2
for p being Element of dom t holds t | p is Element of A2
let X be non-empty ManySortedSet of S; for A2 being X,S -terms all_vars_including inheriting_operations MSAlgebra over S
for t being Element of A2
for p being Element of dom t holds t | p is Element of A2
let A2 be X,S -terms all_vars_including inheriting_operations MSAlgebra over S; for t being Element of A2
for p being Element of dom t holds t | p is Element of A2
set A = A2;
let t be Element of A2; for p being Element of dom t holds t | p is Element of A2
defpred S1[ Nat] means for p being Element of dom t st len p = $1 holds
t | p is Element of A2;
A1:
S1[ 0 ]
A2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A3:
S1[
i]
;
S1[i + 1]
let p be
Element of
dom t;
( len p = i + 1 implies t | p is Element of A2 )
assume A4:
len p = i + 1
;
t | p is Element of A2
then consider q being
FinSequence,
a being
object such that A5:
p = q ^ <*a*>
by FINSEQ_2:18;
<*a*> is
FinSequence of
NAT
by A5, FINSEQ_1:36;
then
rng <*a*> c= NAT
by FINSEQ_1:def 4;
then
{a} c= NAT
by FINSEQ_1:39;
then reconsider a =
a as
Element of
NAT by ZFMISC_1:31;
len <*a*> = 1
by FINSEQ_1:40;
then A6:
len p = (len q) + 1
by A5, FINSEQ_1:22;
reconsider q =
q as
FinSequence of
NAT by A5, FINSEQ_1:36;
reconsider q =
q as
Element of
dom t by A5, TREES_1:21;
t is
Term of
S,
X
by Th42;
then reconsider tq =
t | q,
tp =
t | p as
Term of
S,
X by MSATERM:29;
A7:
dom tq = (dom t) | q
by TREES_2:def 10;
then
(
<*a*> in dom tq &
{} in dom tq )
by A5, TREES_1:22, TREES_1:def 6;
then
not
tq is
trivial
by ZFMISC_1:def 10;
then
tq is
CompoundTerm of
S,
X
by MSATERM:28;
then
tq . {} in [: the carrier' of S,{ the carrier of S}:]
by MSATERM:def 6;
then consider o,
s being
object such that A8:
(
o in the
carrier' of
S &
s in { the carrier of S} &
tq . {} = [o,s] )
by ZFMISC_1:def 2;
reconsider o =
o as
OperSymbol of
S by A8;
A9:
s = the
carrier of
S
by A8, TARSKI:def 1;
then consider arg being
ArgumentSeq of
Sym (
o,
X)
such that A10:
tq = [o, the carrier of S] -tree arg
by A8, MSATERM:10;
(
<*a*> in dom tq &
dom tq = tree (doms arg) &
<*a*> <> {} )
by A7, A5, A10, TREES_1:def 6, TREES_4:10;
then consider n being
Nat,
e being
FinSequence such that A11:
(
n < len (doms arg) &
e in (doms arg) . (n + 1) &
<*a*> = <*n*> ^ e )
by TREES_3:def 15;
A12:
a =
<*a*> . 1
.=
n
by A11, FINSEQ_1:41
;
A13:
Free (
S,
X)
= FreeMSA X
by MSAFREE3:31;
A14:
tq is
Element of
A2
by A3, A6, A4;
(
Sym (
o,
X)
==> roots arg &
arg is
FinSequence of
TS (DTConMSA X) )
by MSATERM:21, MSATERM:def 1;
then
(DenOp (o,X)) . arg = (Sym (o,X)) -tree arg
by MSAFREE:def 12;
then A15:
(Den (o,(Free (S,X)))) . arg = tq
by A10, A13, MSAFREE:def 13;
the_sort_of tq = the_result_sort_of o
by A8, A9, MSATERM:17;
then
(Den (o,(Free (S,X)))) . arg in FreeSort (
X,
(the_result_sort_of o))
by A15, MSATERM:def 5;
then
(Den (o,(Free (S,X)))) . arg in the
Sorts of
(Free (S,X)) . (the_result_sort_of o)
by A13, MSAFREE:def 11;
then A16:
(Den (o,(Free (S,X)))) . arg in the
Sorts of
A2 . (the_result_sort_of o)
by A14, A15, Th43;
reconsider r =
{} as
Element of
dom tq by TREES_1:22;
A17:
(
tp = tq | <*a*> &
a < len arg )
by A5, A11, A12, TREES_3:38, TREES_9:3;
then A18:
(
tp = arg . (a + 1) &
a + 1
in dom arg )
by Lm2, A10, TREES_4:def 4;
reconsider ar =
arg as
Element of
Args (
o,
(Free (S,X)))
by A13, INSTALG1:1;
(
ar in Args (
o,
A2) &
dom the
Arity of
S = the
carrier' of
S )
by A16, Def8, FUNCT_2:def 1;
then
arg in H1( the
Sorts of
A2 # ,
the_arity_of o)
by FUNCT_1:13;
then A19:
arg in product ( the Sorts of A2 * (the_arity_of o))
by FINSEQ_2:def 5;
then A20:
dom arg = dom ( the Sorts of A2 * (the_arity_of o))
by CARD_3:9;
dom ( the Sorts of A2 * (the_arity_of o)) = dom (the_arity_of o)
by PARTFUN1:def 2;
then
(the_arity_of o) . (a + 1) in rng (the_arity_of o)
by A18, A20, FUNCT_1:def 3;
then reconsider s =
(the_arity_of o) . (a + 1) as
SortSymbol of
S ;
tp in ( the Sorts of A2 * (the_arity_of o)) . (a + 1)
by A18, A19, A20, CARD_3:9;
then
tp is
Element of the
Sorts of
A2 . s
by A17, Lm2, A20, FUNCT_1:12;
hence
t | p is
Element of
A2
;
verum
end;
A21:
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A2);
let p be Element of dom t; t | p is Element of A2
len p = len p
;
hence
t | p is Element of A2
by A21; verum