set X = the Sorts of F2() (\/) F3();
set G = DTConMSA ( the Sorts of F2() (\/) F3());
A4:
for nt being Symbol of (DTConMSA ( the Sorts of F2() (\/) F3()))
for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() (\/) F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() (\/) F3())) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]
proof
let nt be
Symbol of
(DTConMSA ( the Sorts of F2() (\/) F3()));
for ts being FinSequence of TS (DTConMSA ( the Sorts of F2() (\/) F3())) st nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() (\/) F3())) st t in rng ts holds
P1[t] ) holds
P1[nt -tree ts]let ts be
FinSequence of
TS (DTConMSA ( the Sorts of F2() (\/) F3()));
( nt ==> roots ts & ( for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() (\/) F3())) st t in rng ts holds
P1[t] ) implies P1[nt -tree ts] )
assume that A5:
nt ==> roots ts
and A6:
for
t being
DecoratedTree of the
carrier of
(DTConMSA ( the Sorts of F2() (\/) F3())) st
t in rng ts holds
P1[
t]
;
P1[nt -tree ts]
nt in { s where s is Symbol of (DTConMSA ( the Sorts of F2() (\/) F3())) : ex n being FinSequence st s ==> n }
by A5;
then reconsider sy =
nt as
NonTerminal of
(DTConMSA ( the Sorts of F2() (\/) F3())) by LANG1:def 3;
reconsider p =
ts as
FinSequence of
F1()
-Terms ( the Sorts of F2() (\/) F3()) ;
sy in [: the carrier' of F1(),{ the carrier of F1()}:]
by Lm5;
then consider o being
OperSymbol of
F1(),
x2 being
Element of
{ the carrier of F1()} such that A7:
sy = [o,x2]
by DOMAIN_1:1;
A8:
[o, the carrier of F1()] = Sym (
o,
( the Sorts of F2() (\/) F3()))
by MSAFREE:def 9;
A9:
x2 = the
carrier of
F1()
by TARSKI:def 1;
then
ts is
SubtreeSeq of
Sym (
o,
( the Sorts of F2() (\/) F3()))
by A5, A7, A8, DTCONSTR:def 6;
then reconsider p =
p as
ArgumentSeq of
Sym (
o,
( the Sorts of F2() (\/) F3()))
by Def2;
for
t being
c-Term of
F2(),
F3() st
t in rng p holds
P1[
t]
by A6;
hence
P1[
nt -tree ts]
by A3, A7, A9, A8;
verum
end;
A10:
for s being Symbol of (DTConMSA ( the Sorts of F2() (\/) F3())) st s in Terminals (DTConMSA ( the Sorts of F2() (\/) F3())) holds
P1[ root-tree s]
for t being DecoratedTree of the carrier of (DTConMSA ( the Sorts of F2() (\/) F3())) st t in TS (DTConMSA ( the Sorts of F2() (\/) F3())) holds
P1[t]
from DTCONSTR:sch 7(A10, A4);
hence
for t being c-Term of F2(),F3() holds P1[t]
; verum