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