let a, b be set ; ( a <> b implies Lang (SingleGrammar (a,b)) = {<*b*>} )
set E = SingleGrammar (a,b);
A1:
the InitialSym of (SingleGrammar (a,b)) = a
by Def8;
the carrier of (SingleGrammar (a,b)) = {a,b}
by Def8;
then reconsider x = a, y = b as Symbol of (SingleGrammar (a,b)) by TARSKI:def 2;
A2:
the Rules of (SingleGrammar (a,b)) = {[a,<*b*>]}
by Def8;
then
[a,<*b*>] in the Rules of (SingleGrammar (a,b))
by TARSKI:def 1;
then
the InitialSym of (SingleGrammar (a,b)) ==> <*y*>
by A1;
then A3:
<*y*> is_derivable_from <* the InitialSym of (SingleGrammar (a,b))*>
by Th3, Th7;
assume A4:
a <> b
; Lang (SingleGrammar (a,b)) = {<*b*>}
then A5:
Terminals (SingleGrammar (a,b)) = {b}
by Th12;
thus
Lang (SingleGrammar (a,b)) c= {<*b*>}
XBOOLE_0:def 10 {<*b*>} c= Lang (SingleGrammar (a,b))proof
let c be
object ;
TARSKI:def 3 ( not c in Lang (SingleGrammar (a,b)) or c in {<*b*>} )
assume
c in Lang (SingleGrammar (a,b))
;
c in {<*b*>}
then consider p being
String of
(SingleGrammar (a,b)) such that A6:
c = p
and A7:
rng p c= Terminals (SingleGrammar (a,b))
and A8:
p is_derivable_from <* the InitialSym of (SingleGrammar (a,b))*>
;
consider q being
FinSequence such that A9:
len q >= 1
and A10:
q . 1
= <* the InitialSym of (SingleGrammar (a,b))*>
and A11:
q . (len q) = p
and A12:
for
i being
Element of
NAT st
i >= 1 &
i < len q holds
ex
a,
b being
String of
(SingleGrammar (a,b)) st
(
q . i = a &
q . (i + 1) = b &
a ==> b )
by A8;
then A13:
len q > 1
by A1, A9, A10, A11, XXREAL_0:1;
then consider n,
m being
String of
(SingleGrammar (a,b)) such that A14:
q . 1
= n
and A15:
q . (1 + 1) = m
and A16:
n ==> m
by A12;
x ==> m
by A1, A10, A14, A16, Th4;
then
[x,m] in {[a,<*b*>]}
by A2;
then
[x,m] = [a,<*b*>]
by TARSKI:def 1;
then A17:
m = <*b*>
by XTUPLE_0:1;
A18:
now not 2 < len qassume
2
< len q
;
contradictionthen consider k,
l being
String of
(SingleGrammar (a,b)) such that A19:
q . 2
= k
and
q . (2 + 1) = l
and A20:
k ==> l
by A12;
y ==> l
by A15, A17, A19, A20, Th4;
then
[y,l] in {[a,<*b*>]}
by A2;
then
[y,l] = [a,<*b*>]
by TARSKI:def 1;
hence
contradiction
by A4, XTUPLE_0:1;
verum end;
len q >= 1
+ 1
by A13, NAT_1:13;
then
c = <*b*>
by A6, A11, A15, A17, A18, XXREAL_0:1;
hence
c in {<*b*>}
by TARSKI:def 1;
verum
end;
let c be object ; TARSKI:def 3 ( not c in {<*b*>} or c in Lang (SingleGrammar (a,b)) )
assume
c in {<*b*>}
; c in Lang (SingleGrammar (a,b))
then A21:
c = <*b*>
by TARSKI:def 1;
rng <*b*> = {b}
by FINSEQ_1:38;
hence
c in Lang (SingleGrammar (a,b))
by A5, A21, A3; verum