let D be non empty set ; Lang (TotalGrammar D) = D *
set T = TotalGrammar D;
set I = <* the InitialSym of (TotalGrammar D)*>;
defpred S1[ Nat] means for p being String of (TotalGrammar D) st len p = $1 & p in D * holds
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>;
A1:
D c= succ D
by XBOOLE_1:7;
A2:
the Rules of (TotalGrammar D) = { [D,<*d,D*>] where d is Element of D : d = d } \/ {[D,{}]}
by Def10;
A3:
the InitialSym of (TotalGrammar D) = D
by Def10;
A4:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A5:
for
p being
String of
(TotalGrammar D) st
len p = k &
p in D * holds
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
;
S1[k + 1]
let p be
String of
(TotalGrammar D);
( len p = k + 1 & p in D * implies p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*> )
assume that A6:
len p = k + 1
and A7:
p in D *
;
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
consider q being
FinSequence,
a being
set such that A8:
p = q ^ <*a*>
and A9:
len q = k
by A6, TREES_2:3;
A10:
rng <*a*> = {a}
by FINSEQ_1:38;
<*a*> is
FinSequence of the
carrier of
(TotalGrammar D)
by A8, FINSEQ_1:36;
then A11:
{a} c= the
carrier of
(TotalGrammar D)
by A10, FINSEQ_1:def 4;
A12:
q is
FinSequence of the
carrier of
(TotalGrammar D)
by A8, FINSEQ_1:36;
A13:
p is
FinSequence of
D
by A7, FINSEQ_1:def 11;
then A14:
q is
FinSequence of
D
by A8, FINSEQ_1:36;
<*a*> is
FinSequence of
D
by A8, A13, FINSEQ_1:36;
then A15:
{a} c= D
by A10, FINSEQ_1:def 4;
reconsider q =
q as
String of
(TotalGrammar D) by A12, FINSEQ_1:def 11;
reconsider a =
a as
Element of
D by A15, ZFMISC_1:31;
reconsider x =
a as
Symbol of
(TotalGrammar D) by A11, ZFMISC_1:31;
[D,<*a,D*>] in { [D,<*d,D*>] where d is Element of D : d = d }
;
then
[D,<*a,D*>] in the
Rules of
(TotalGrammar D)
by A2, XBOOLE_0:def 3;
then
the
InitialSym of
(TotalGrammar D) ==> <*x, the InitialSym of (TotalGrammar D)*>
by A3;
then
<* the InitialSym of (TotalGrammar D)*> ==> <*x, the InitialSym of (TotalGrammar D)*>
by Th3;
then A16:
q ^ <* the InitialSym of (TotalGrammar D)*> ==> q ^ <*x, the InitialSym of (TotalGrammar D)*>
by Th5;
<*x, the InitialSym of (TotalGrammar D)*> = <*x*> ^ <* the InitialSym of (TotalGrammar D)*>
by FINSEQ_1:def 9;
then
q ^ <* the InitialSym of (TotalGrammar D)*> ==> p ^ <* the InitialSym of (TotalGrammar D)*>
by A8, A16, FINSEQ_1:32;
then A17:
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from q ^ <* the InitialSym of (TotalGrammar D)*>
by Th7;
q in D *
by A14, FINSEQ_1:def 11;
then
q ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
by A5, A9;
hence
p ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
by A17, Th8;
verum
end;
[D,{}] in {[D,{}]}
by TARSKI:def 1;
then
[D,{}] in the Rules of (TotalGrammar D)
by A2, XBOOLE_0:def 3;
then
the InitialSym of (TotalGrammar D) ==> <*> the carrier of (TotalGrammar D)
by A3;
then A18:
<* the InitialSym of (TotalGrammar D)*> ==> <*> the carrier of (TotalGrammar D)
by Th3;
A19:
Terminals (TotalGrammar D) = D
by Th16;
thus
Lang (TotalGrammar D) c= D *
XBOOLE_0:def 10 D * c= Lang (TotalGrammar D)
let a be object ; TARSKI:def 3 ( not a in D * or a in Lang (TotalGrammar D) )
assume A22:
a in D *
; a in Lang (TotalGrammar D)
then reconsider a = a as FinSequence of D by FINSEQ_1:def 11;
the carrier of (TotalGrammar D) = succ D
by Def10;
then
rng a c= the carrier of (TotalGrammar D)
by A1;
then
a is FinSequence of the carrier of (TotalGrammar D)
by FINSEQ_1:def 4;
then reconsider n = a as String of (TotalGrammar D) by FINSEQ_1:def 11;
n ^ {} = n
by FINSEQ_1:34;
then
n ^ <* the InitialSym of (TotalGrammar D)*> ==> n
by A18, Th5;
then A23:
n is_derivable_from n ^ <* the InitialSym of (TotalGrammar D)*>
by Th7;
A24:
S1[ 0 ]
A25:
for k being Nat holds S1[k]
from NAT_1:sch 2(A24, A4);
len n = len n
;
then
n ^ <* the InitialSym of (TotalGrammar D)*> is_derivable_from <* the InitialSym of (TotalGrammar D)*>
by A25, A22;
then A26:
n is_derivable_from <* the InitialSym of (TotalGrammar D)*>
by A23, Th8;
rng a c= D
;
hence
a in Lang (TotalGrammar D)
by A19, A26; verum