:: Context-Free Grammar - Part 1
:: by Patricia L. Carlson and Grzegorz Bancerek
::
:: Received February 21, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, STRUCT_0, RELAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1,
TDGROUP, TARSKI, ORDINAL4, ARYTM_3, CARD_1, FUNCT_1, XXREAL_0, NAT_1,
ZFMISC_1, ORDINAL1, FINSET_1, LANG1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
NAT_1, DOMAIN_1, RELAT_1, STRUCT_0, FUNCT_1, FINSEQ_1, FINSET_1,
RELSET_1, PARTFUN1, FUNCT_2, FINSEQ_2, XXREAL_0, PRE_POLY;
constructors PARTFUN1, DOMAIN_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_2, STRUCT_0,
RELSET_1, PRE_POLY;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, FINSET_1,
XXREAL_0, XREAL_0, FINSEQ_1, STRUCT_0, ORDINAL1, CARD_1, RELSET_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions XBOOLE_0, TARSKI, RELAT_1, STRUCT_0;
equalities ORDINAL1;
expansions TARSKI;
theorems TARSKI, ZFMISC_1, RELAT_1, FINSEQ_1, NAT_1, RELSET_1, TREES_2,
FUNCT_2, FINSEQ_3, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1,
XTUPLE_0;
schemes NAT_1, FUNCT_2;
begin
:: Grammar structure is introduced as triple (S, I, R) where S is
:: a set of non-terminal and terminal symbols, I is an initial symbol,
:: and R is a set of rules (ordered pairs).
definition
struct(1-sorted) DTConstrStr (# carrier -> set, Rules -> Relation of the
carrier, (the carrier)* #);
end;
registration
cluster non empty strict for DTConstrStr;
existence
proof
set A = the non empty set,P = the Relation of A,A*;
take DTConstrStr(#A,P#);
thus the carrier of DTConstrStr(#A,P#) is non empty;
thus thesis;
end;
end;
definition
struct(DTConstrStr) GrammarStr (# carrier -> set, InitialSym -> Element of
the carrier, Rules -> Relation of the carrier, (the carrier)* #);
end;
registration
cluster non empty for GrammarStr;
existence
proof
set A = the non empty set,P = the Relation of A,A*,I = the Element of A;
take GrammarStr(#A,I,P#);
thus the carrier of GrammarStr(#A,I,P#) is non empty;
end;
end;
definition
let G be DTConstrStr;
mode Symbol of G is Element of G;
mode String of G is Element of (the carrier of G)*;
end;
reserve G for non empty DTConstrStr,
s for Symbol of G,
n,m for String of G;
definition
let G,s;
let n be FinSequence;
pred s ==> n means
[s,n] in the Rules of G;
end;
definition
let G;
func Terminals G -> set equals
{ s : not ex n being FinSequence st s ==> n};
coherence;
func NonTerminals G -> set equals
{ s : ex n being FinSequence st s ==> n};
coherence;
end;
theorem
Terminals(G) \/ NonTerminals(G) = the carrier of G
proof
thus Terminals G \/ NonTerminals G c= the carrier of G
proof
let a be object;
assume a in Terminals G \/ NonTerminals G;
then a in Terminals G or a in NonTerminals G by XBOOLE_0:def 3;
then
(ex s st a = s & not ex n being FinSequence st s ==> n) or ex s st a =
s & ex n being FinSequence st s ==> n;
hence thesis;
end;
let a be object;
assume a in the carrier of G;
then reconsider s = a as Symbol of G;
not (ex n being FinSequence st s ==> n) or ex n being FinSequence st s ==> n;
then a in Terminals G or a in NonTerminals G;
hence thesis by XBOOLE_0:def 3;
end;
definition
let G,n,m;
pred n ==> m means
ex n1,n2,n3 being String of G, s st n = n1^<*s*>^n2 & m =
n1^n3^n2 & s ==> n3;
end;
reserve n1,n2,n3 for String of G;
theorem
s ==> n implies n1^<*s*>^n2 ==> n1^n^n2;
theorem Th3:
s ==> n implies <*s*> ==> n
proof
assume
A1: s ==> n;
take n1 = <*>(the carrier of G), n2 = <*>(the carrier of G), n3 = n, s;
thus <*s*> = n1^<*s*> by FINSEQ_1:34
.= n1^<*s*>^n2 by FINSEQ_1:34;
thus n = n1^n3 by FINSEQ_1:34
.= n1^n3^n2 by FINSEQ_1:34;
thus thesis by A1;
end;
theorem Th4:
<*s*> ==> n implies s ==> n
proof
given n1,n2,n3 being String of G, t being Symbol of G such that
A1: <*s*> = n1^<*t*>^n2 and
A2: n = n1^n3^n2 and
A3: t ==> n3;
A4: len <*t*> = 1 by FINSEQ_1:40;
A5: len (n1^<*t*>) = len n1 + len <*t*> by FINSEQ_1:22;
len <*s*> = len (n1^<*t*>) + len n2 by A1,FINSEQ_1:22;
then
A6: 1+0 = 1+(len n1+len n2) by A4,A5,FINSEQ_1:40;
then
A7: n2 = {} by NAT_1:7;
A8: n3^{} = n3 by FINSEQ_1:34;
A9: {}^n3 = n3 by FINSEQ_1:34;
A10: <*s*>.1 = s;
A11: <*t*>^{} = <*t*> by FINSEQ_1:34;
A12: {}^<*t*> = <*t*> by FINSEQ_1:34;
n1 = {} by A6,NAT_1:7;
hence thesis by A1,A2,A3,A7,A12,A11,A9,A8,A10,FINSEQ_1:40;
end;
theorem Th5:
n1 ==> n2 implies n^n1 ==> n^n2 & n1^n ==> n2^n
proof
given m1,m2,m3 being String of G, s being Symbol of G such that
A1: n1 = m1^<*s*>^m2 and
A2: n2 = m1^m3^m2 and
A3: s ==> m3;
thus n^n1 ==> n^n2
proof
take n^m1, m2, m3, s;
thus n^n1 = n^(m1^<*s*>)^m2 by A1,FINSEQ_1:32
.= n^m1^<*s*>^m2 by FINSEQ_1:32;
thus n^n2 = n^(m1^m3)^m2 by A2,FINSEQ_1:32
.= n^m1^m3^m2 by FINSEQ_1:32;
thus thesis by A3;
end;
take m1, m2^n, m3, s;
thus thesis by A1,A2,A3,FINSEQ_1:32;
end;
definition
let G, n, m;
pred m is_derivable_from n means
ex p being FinSequence st len p >= 1
& p.1 = n & p.len p = m & for i being Element of NAT st i >= 1 & i < len p ex a
,b being String of G st p.i = a & p.(i+1) = b & a ==> b;
end;
theorem Th6:
n is_derivable_from n
proof
take p = <*n*>;
len p = 1 by FINSEQ_1:40;
hence len p >= 1 & p.1 = n & p.len p = n;
let i be Element of NAT;
assume that
A1: i >= 1 and
A2: i < len p;
thus thesis by A1,A2,FINSEQ_1:40;
end;
theorem Th7:
n ==> m implies m is_derivable_from n
proof
assume
A1: n ==> m;
take p = <*n,m*>;
A2: len p = 2 by FINSEQ_1:44;
hence len p >= 1 & p.1 = n & p.(len p) = m;
let i be Element of NAT;
assume that
A3: i >= 1 and
A4: i < len p;
take a = n, b = m;
2 = 1 + 1;
then i <= 1 by A2,A4,NAT_1:13;
then
A5: i = 1 by A3,XXREAL_0:1;
hence p.i = a;
thus p.(i+1) = b by A5;
thus thesis by A1;
end;
theorem Th8:
n1 is_derivable_from n2 & n2 is_derivable_from n3 implies n1
is_derivable_from n3
proof
given p1 being FinSequence such that
A1: len p1 >= 1 and
A2: p1.1 = n2 and
A3: p1.(len p1) = n1 and
A4: for i being Element of NAT st i >= 1 & i < len p1 ex a,b being
String of G st p1.i = a & p1.(i+1) = b & a ==> b;
given p2 being FinSequence such that
A5: len p2 >= 1 and
A6: p2.1 = n3 and
A7: p2.(len p2) = n2 and
A8: for i being Element of NAT st i >= 1 & i < len p2 ex a,b being
String of G st p2.i = a & p2.(i+1) = b & a ==> b;
p2 <> {} by A5;
then consider q being FinSequence, x being object such that
A9: p2 = q^<*x*> by FINSEQ_1:46;
take p = q^p1;
A10: 1+len q >= 1 by NAT_1:11;
A11: len p = len q+len p1 by FINSEQ_1:22;
then len p >= 1+len q by A1,XREAL_1:7;
hence len p >= 1 by A10,XXREAL_0:2;
now
per cases;
suppose
A12: q = {};
then
A13: p = p1 by FINSEQ_1:34;
p2 = <*x*> by A9,A12,FINSEQ_1:34;
hence p.1 = n3 by A2,A6,A7,A13,FINSEQ_1:40;
end;
suppose
A14: q <> {};
A15: 0+1 = 1;
len q > 0 by A14,NAT_1:2;
then len q >= 1 by A15,NAT_1:13;
then
A16: 1 in dom q by FINSEQ_3:25;
then p.1 = q.1 by FINSEQ_1:def 7;
hence p.1 = n3 by A6,A9,A16,FINSEQ_1:def 7;
end;
end;
hence p.1 = n3;
len p1 in dom p1 by A1,FINSEQ_3:25;
hence p.(len p) = n1 by A3,A11,FINSEQ_1:def 7;
let i be Element of NAT such that
A17: i >= 1 and
A18: i < len p;
len <*x*> = 1 by FINSEQ_1:40;
then
A19: len p2 = len q + 1 by A9,FINSEQ_1:22;
now
per cases by XXREAL_0:1;
suppose
A20: i+1 = len p2;
A21: 1 in dom p1 by A1,FINSEQ_3:25;
i < len p2 by A20,NAT_1:13;
then consider a,b being String of G such that
A22: p2.i = a and
A23: p2.(i+1) = b and
A24: a ==> b by A8,A17;
take a, b;
A25: i in dom q by A19,A17,A20,FINSEQ_3:25;
then p2.i = q.i by A9,FINSEQ_1:def 7;
hence p.i = a & p.(i+1) = b & a ==> b by A2,A7,A19,A20,A22,A23,A24,A21
,A25,FINSEQ_1:def 7;
end;
suppose
i+1 > len p2;
then i >= len p2 by NAT_1:13;
then consider j being Nat such that
A26: i = len p2 + j by NAT_1:10;
reconsider j as Element of NAT by ORDINAL1:def 12;
A27: i = len q +(1+j) by A19,A26;
then
A28: 1+j < len p1 by A11,A18,XREAL_1:6;
then consider a,b being String of G such that
A29: p1.(1+j) = a and
A30: p1.(1+j+1) = b and
A31: a ==> b by A4,NAT_1:11;
take a, b;
A32: 1+j+1 >= 1 by NAT_1:11;
1+j >= 1 by NAT_1:11;
then
A33: 1+j in dom p1 by A28,FINSEQ_3:25;
1+j+1 <= len p1 by A28,NAT_1:13;
then
A34: 1+j+1 in dom p1 by A32,FINSEQ_3:25;
i+1 = len q +(1+j+1) by A19,A26;
hence p.i = a & p.(i+1) = b & a ==> b by A27,A29,A30,A31,A33,A34,
FINSEQ_1:def 7;
end;
suppose
A35: i+1 < len p2;
A36: 1 <= 1+i by NAT_1:11;
i+1 <= len q by A19,A35,NAT_1:13;
then
A37: i+1 in dom q by A36,FINSEQ_3:25;
then
A38: p.(i+1) = q.(i+1) by FINSEQ_1:def 7;
i < len p2 by A35,NAT_1:13;
then consider a,b being String of G such that
A39: p2.i = a and
A40: p2.(i+1) = b and
A41: a ==> b by A8,A17;
take a, b;
i <= len q by A19,A35,XREAL_1:6;
then
A42: i in dom q by A17,FINSEQ_3:25;
then p.i = q.i by FINSEQ_1:def 7;
hence p.i = a & p.(i+1) = b & a ==> b by A9,A39,A40,A41,A42,A37,A38,
FINSEQ_1:def 7;
end;
end;
hence thesis;
end;
:: Define language
definition
let G be non empty GrammarStr;
func Lang(G) -> set equals
{a where a is Element of (the carrier of G)*: rng a c=
Terminals(G) & a is_derivable_from <*the InitialSym of G*>};
coherence;
end;
theorem
for G being non empty GrammarStr, n being String of G holds n in Lang(
G) iff rng n c= Terminals(G) & n is_derivable_from <*the InitialSym of G*>
proof
let G be non empty GrammarStr, n be String of G;
now
assume n in Lang G;
then ex a being Element of (the carrier of G)* st n = a & rng a c=
Terminals(G) & a is_derivable_from <*the InitialSym of G*>;
hence rng n c= Terminals(G) & n is_derivable_from <*the InitialSym of G*>;
end;
hence thesis;
end;
:: GrammarStr(#{a},a,{[a,{}{a}]}#) -> Lang = {{}}
:: GrammarStr(#{a,b},a,{[a,<*b*>]}#) -> Lang = {b}
:: GrammarStr(#{a,b},a,{[a,{}{a}],[a,<*a,b*>]}#) -> Lang = {{}, b, bb, ...}
:: GrammarStr(#{a,b,c},a,{[a,<*b*>}],[a,<*c*>]}#) -> Lang = {b, c}
definition
let D,E be non empty set, a be Element of [:D,E:];
redefine func {a} -> Relation of D,E; :: redefines { (TARSKI, definition)
coherence
proof
{a} c= [:D,E:];
hence thesis;
end;
let b be Element of [:D,E:];
redefine func {a,b} -> Relation of D,E; :: redefines { (TARSKI, definition)
coherence
proof
{a,b} c= [:D,E:];
hence thesis;
end;
end;
definition
let a be set;
func EmptyGrammar a -> strict GrammarStr means
:Def7:
the carrier of it = {a } & the Rules of it = {[a,{}]};
existence
proof
reconsider S = a as Element of {a} by TARSKI:def 1;
take GrammarStr(#{a}, S, {[S,<*>{a}]}#);
thus thesis;
end;
uniqueness
proof
let G1, G2 be strict GrammarStr such that
A1: the carrier of G1 = {a} and
A2: the Rules of G1 = {[a,{}]} and
A3: the carrier of G2 = {a} and
A4: the Rules of G2 = {[a,{}]};
the InitialSym of G1 = a by A1,TARSKI:def 1;
hence thesis by A1,A2,A3,A4,TARSKI:def 1;
end;
let b be set;
func SingleGrammar(a,b) -> strict GrammarStr means
:Def8:
the carrier of it
= {a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b*>]};
existence
proof
reconsider S = a, x = b as Element of {a,b} by TARSKI:def 2;
take GrammarStr(#{a,b}, S, {[S,<*x*>]}#);
thus thesis;
end;
uniqueness;
func IterGrammar(a,b) -> strict GrammarStr means
:Def9:
the carrier of it =
{a,b} & the InitialSym of it = a & the Rules of it = {[a,<*b,a*>],[a,{}]};
existence
proof
reconsider S = a, x = b as Element of {a,b} by TARSKI:def 2;
take GrammarStr(#{a,b}, S, {[S,<*x,S*>], [S,<*>{a,b}]}#);
thus thesis;
end;
uniqueness;
end;
registration
let a be set;
cluster EmptyGrammar a -> non empty;
coherence
proof
the carrier of EmptyGrammar a = {a} by Def7;
hence the carrier of EmptyGrammar a is non empty;
end;
let b be set;
cluster SingleGrammar(a,b) -> non empty;
coherence
proof
the carrier of SingleGrammar(a,b) = {a,b} by Def8;
hence the carrier of SingleGrammar(a,b) is non empty;
end;
cluster IterGrammar(a,b) -> non empty;
coherence
proof
the carrier of IterGrammar(a,b) = {a,b} by Def9;
hence the carrier of IterGrammar(a,b) is non empty;
end;
end;
definition
let D be non empty set;
func TotalGrammar D -> strict GrammarStr means
: Def10:
the carrier of it =
succ D & the InitialSym of it = D & the Rules of it = {[D,<*d,D*>] where d is
Element of D: d = d} \/ {[D,{}]};
existence
proof
reconsider E = succ D as non empty set;
D in {D} by TARSKI:def 1;
then reconsider S = D as Element of E by XBOOLE_0:def 3;
set R = {[S,<*d,S*>] where d is Element of D: d = d};
R c= [:E,E*:]
proof
let a be object;
assume a in R;
then consider d being Element of D such that
A1: a = [S,<*d,S*>] and
d = d;
reconsider d as Element of E by XBOOLE_0:def 3;
a = [S,<*d,S*>] by A1;
hence thesis;
end;
then reconsider R as Relation of E, E*;
take GrammarStr(#E, S, R \/ {[S,<*>E]}#);
thus thesis;
end;
uniqueness;
end;
registration
let D be non empty set;
cluster TotalGrammar D -> non empty;
coherence
proof
the carrier of TotalGrammar D = succ D by Def10;
hence the carrier of TotalGrammar D is non empty;
end;
end;
reserve a,b,c for set,
D for non empty set,
d for Element of D;
theorem Th10:
Terminals EmptyGrammar a = {}
proof
set E = EmptyGrammar a;
set b = the Element of Terminals E;
the Rules of E = {[a,{}]} by Def7;
then
A1: [a,{}] in the Rules of E by TARSKI:def 1;
assume not thesis;
then b in Terminals E;
then consider s being Symbol of E such that
b = s and
A2: not ex n being FinSequence st s ==> n;
the carrier of E = {a} by Def7;
then s = a by TARSKI:def 1;
then s ==> <*>the carrier of E by A1;
hence contradiction by A2;
end;
theorem Th11:
Lang EmptyGrammar a = {{}}
proof
set E = EmptyGrammar a;
A1: Terminals E = {} by Th10;
thus Lang E c= {{}}
proof
let b be object;
assume b in Lang E;
then ex p being String of E st b = p & rng p c= Terminals E & p
is_derivable_from <*the InitialSym of E*>;
then b = {} by A1;
hence thesis by TARSKI:def 1;
end;
let b be object;
assume b in {{}};
then
A2: b = {} by TARSKI:def 1;
the Rules of E = {[a,{}]} by Def7;
then
A3: [a,{}] in the Rules of E by TARSKI:def 1;
the carrier of E = {a} by Def7;
then a = the InitialSym of E by TARSKI:def 1;
then the InitialSym of E ==> <*> the carrier of E by A3;
then
A4: <*> the carrier of E is_derivable_from <*the InitialSym of E*> by Th3,Th7;
rng {} = {};
hence thesis by A1,A2,A4;
end;
theorem Th12:
a <> b implies Terminals SingleGrammar(a,b) = {b}
proof
set E = SingleGrammar(a,b);
A1: the Rules of E = {[a,<*b*>]} by Def8;
A2: the carrier of E = {a,b} by Def8;
then reconsider x = a, y = b as Symbol of E by TARSKI:def 2;
assume
A3: a <> b;
A4: now
let n be FinSequence;
assume y ==> n;
then [y,n] in {[a,<*b*>]} by A1;
then [y,n] = [a,<*b*>] by TARSKI:def 1;
hence contradiction by A3,XTUPLE_0:1;
end;
[x,<*y*>] in the Rules of E by A1,TARSKI:def 1;
then
A5: x ==> <*y*>;
thus Terminals E c= {b}
proof
let c be object;
assume c in Terminals E;
then consider s being Symbol of E such that
A6: c = s and
A7: not ex n being FinSequence st s ==> n;
s <> x by A5,A7;
then c = b by A2,A6,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
let c be object;
assume c in {b};
then c = b by TARSKI:def 1;
hence thesis by A4;
end;
theorem
a <> b implies Lang SingleGrammar(a,b) = {<*b*>}
proof
set E = SingleGrammar(a,b);
A1: the InitialSym of E = a by Def8;
the carrier of E = {a,b} by Def8;
then reconsider x = a, y = b as Symbol of E by TARSKI:def 2;
A2: the Rules of E = {[a,<*b*>]} by Def8;
then [a,<*b*>] in the Rules of E by TARSKI:def 1;
then the InitialSym of E ==> <*y*> by A1;
then
A3: <*y*> is_derivable_from <*the InitialSym of E*> by Th3,Th7;
assume
A4: a <> b;
then
A5: Terminals E = {b} by Th12;
thus Lang E c= {<*b*>}
proof
let c be object;
assume c in Lang E;
then consider p being String of E such that
A6: c = p and
A7: rng p c= Terminals E and
A8: p is_derivable_from <*the InitialSym of E*>;
consider q being FinSequence such that
A9: len q >= 1 and
A10: q.1 = <*the InitialSym of E*> and
A11: q.(len q) = p and
A12: for i being Element of NAT st i >= 1 & i < len q ex a,b being
String of E st q.i = a & q.(i+1) = b & a ==> b by A8;
now
assume p = <*x*>;
then rng p = {x} by FINSEQ_1:38;
then x in rng p by TARSKI:def 1;
hence contradiction by A4,A5,A7,TARSKI:def 1;
end;
then
A13: len q > 1 by A1,A9,A10,A11,XXREAL_0:1;
then consider n, m being String of E 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
assume 2 < len q;
then consider k, l being String of E 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;
end;
len q >= 1+1 by A13,NAT_1:13;
then c = <*b*> by A6,A11,A15,A17,A18,XXREAL_0:1;
hence thesis by TARSKI:def 1;
end;
let c be object;
assume c in {<*b*>};
then
A21: c = <*b*> by TARSKI:def 1;
rng <*b*> = {b} by FINSEQ_1:38;
hence thesis by A5,A21,A3;
end;
theorem Th14:
a <> b implies Terminals IterGrammar(a,b) = {b}
proof
set T = IterGrammar(a,b);
assume
A1: a <> b;
A2: the carrier of T = {a,b} by Def9;
then reconsider x = a, y = b as Symbol of T by TARSKI:def 2;
A3: the Rules of T = {[a,<*b,a*>],[a,{}]} by Def9;
thus Terminals T c= {b}
proof
let c be object;
assume c in Terminals T;
then consider s being Symbol of T such that
A4: c = s and
A5: not ex n being FinSequence st s ==> n;
[a,<*b,a*>] in the Rules of T by A3,TARSKI:def 2;
then x ==> <*y,x*>;
then s <> x by A5;
then c = b by A2,A4,TARSKI:def 2;
hence thesis by TARSKI:def 1;
end;
let c be object;
assume c in {b};
then
A6: b = c by TARSKI:def 1;
assume not thesis;
then consider n being FinSequence such that
A7: y ==> n by A6;
A8: [a,{}] <> [b,n] by A1,XTUPLE_0:1;
[a,<*b,a*>] <> [b,n] by A1,XTUPLE_0:1;
then not [b,n] in {[a,<*b,a*>],[a,{}]} by A8,TARSKI:def 2;
hence thesis by A3,A7;
end;
theorem
a <> b implies Lang IterGrammar(a,b) = {b}*
proof
set T = IterGrammar(a,b);
set I = <*the InitialSym of T*>;
defpred X[Nat] means for p being String of T st len p = $1 & p in
{b}* holds p^I is_derivable_from I;
A1: the carrier of T = {a,b} by Def9;
assume a <> b;
then
A2: Terminals T = {b} by Th14;
thus Lang T c= {b}*
proof
let a be object;
assume a in Lang T;
then consider p being String of T such that
A3: a = p and
A4: rng p c= Terminals T and
p is_derivable_from <*the InitialSym of T*>;
p is FinSequence of {b} by A2,A4,FINSEQ_1:def 4;
hence thesis by A3,FINSEQ_1:def 11;
end;
A5: the InitialSym of T = a by Def9;
A6: the Rules of T = {[a,<*b,a*>],[a,{}]} by Def9;
then [a,{}] in the Rules of T by TARSKI:def 2;
then the InitialSym of T ==> <*> the carrier of T by A5;
then
A7: I ==> <*> the carrier of T by Th3;
A8: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A9: for p being String of T st len p = k & p in {b}* holds p^I
is_derivable_from I;
let p be String of T;
assume that
A10: len p = k+1 and
A11: p in {b}*;
consider q being FinSequence, c 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 T by A12,FINSEQ_1:36;
then
A17: {c} c= the carrier of T 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 as Element of {b} by ZFMISC_1:31;
reconsider x = c as Symbol of T by A17,ZFMISC_1:31;
A18: q is FinSequence of the carrier of T by A12,FINSEQ_1:36;
A19: [a,<*b,a*>] in the Rules of T by A6,TARSKI:def 2;
reconsider q as String of T by A18,FINSEQ_1:def 11;
c = b by TARSKI:def 1;
then the InitialSym of T ==> <*x,the InitialSym of T*> by A5,A19;
then I ==> <*x,the InitialSym of T*> by Th3;
then
A20: q^I ==> q^<*x,the InitialSym of T*> by Th5;
<*x,the InitialSym of T*> = <*x*>^I by FINSEQ_1:def 9;
then q^I ==> p^I by A12,A20,FINSEQ_1:32;
then
A21: p^I is_derivable_from q^I by Th7;
q in {b}* by A16,FINSEQ_1:def 11;
then q^I is_derivable_from I by A9,A13;
hence thesis by A21,Th8;
end;
let c be object;
assume
A22: c in {b}*;
then reconsider 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 T by A1,FINSEQ_1:def 4;
then reconsider n = c as String of T by FINSEQ_1:def 11;
n^{} = n by FINSEQ_1:34;
then n^I ==> n by A7,Th5;
then
A23: n is_derivable_from n^I by Th7;
A24: X[0]
proof
let p be String of T;
assume len p = 0;
then p = {};
then p^I = I by FINSEQ_1:34;
hence thesis by Th6;
end;
A25: for k being Nat holds X[k] from NAT_1:sch 2(A24,A8);
len n = len n;
then n^I is_derivable_from I by A25,A22;
then
A26: n is_derivable_from I by A23,Th8;
rng c c= {b};
hence thesis by A2,A26;
end;
theorem Th16:
Terminals TotalGrammar D = D
proof
set T = TotalGrammar D;
A1: the Rules of T = {[D,<*d,D*>] where d is Element of D: d = d} \/ {[D,{}]
} by Def10;
A2: the carrier of T = succ D by Def10;
thus Terminals T c= D
proof
reconsider b = D as Symbol of T by Def10;
let a be object;
assume a in Terminals T;
then consider s being Symbol of T such that
A3: a = s and
A4: not ex n being FinSequence st s ==> n;
[D,{}] in {[D,{}]} by TARSKI:def 1;
then [D,{}] in the Rules of T by A1,XBOOLE_0:def 3;
then b ==> <*> the carrier of T;
then s <> D by A4;
then not s in {D} by TARSKI:def 1;
hence thesis by A2,A3,XBOOLE_0:def 3;
end;
let a be object;
assume a in D;
then reconsider a as Element of D;
reconsider x = a as Symbol of T by A2,XBOOLE_0:def 3;
assume not thesis;
then consider n being FinSequence such that
A5: x ==> n;
A6: not a in a;
then a <> D;
then [a,n] <> [D,{}] by XTUPLE_0:1;
then
A7: not [a,n] in {[D,{}]} by TARSKI:def 1;
[a,n] in the Rules of T by A5;
then [a,n] in {[D,<*d,D*>]: d = d} by A1,A7,XBOOLE_0:def 3;
then ex d st [a,n] = [D,<*d,D*>] & d = d;
then a = D by XTUPLE_0:1;
hence thesis by A6;
end;
theorem
Lang TotalGrammar D = D*
proof
set T = TotalGrammar D;
set I = <*the InitialSym of T*>;
defpred X[Nat] means for p being String of T st len p = $1 & p in
D* holds p^I is_derivable_from I;
A1: D c= succ D by XBOOLE_1:7;
A2: the Rules of T = {[D,<*d,D*>] where d is Element of D: d = d} \/ {[D,{}]
} by Def10;
A3: the InitialSym of T = D by Def10;
A4: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
A5: for p being String of T st len p = k & p in D* holds p^I
is_derivable_from I;
let p be String of T;
assume that
A6: len p = k+1 and
A7: p in D*;
consider q being FinSequence, a 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 T by A8,FINSEQ_1:36;
then
A11: {a} c= the carrier of T by A10,FINSEQ_1:def 4;
A12: q is FinSequence of the carrier of T 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 as String of T by A12,FINSEQ_1:def 11;
reconsider a as Element of D by A15,ZFMISC_1:31;
reconsider x = a as Symbol of T by A11,ZFMISC_1:31;
[D,<*a,D*>] in {[D,<*d,D*>]: d = d};
then [D,<*a,D*>] in the Rules of T by A2,XBOOLE_0:def 3;
then the InitialSym of T ==> <*x,the InitialSym of T*> by A3;
then I ==> <*x,the InitialSym of T*> by Th3;
then
A16: q^I ==> q^<*x,the InitialSym of T*> by Th5;
<*x,the InitialSym of T*> = <*x*>^I by FINSEQ_1:def 9;
then q^I ==> p^I by A8,A16,FINSEQ_1:32;
then
A17: p^I is_derivable_from q^I by Th7;
q in D* by A14,FINSEQ_1:def 11;
then q^I is_derivable_from I by A5,A9;
hence thesis by A17,Th8;
end;
[D,{}] in {[D,{}]} by TARSKI:def 1;
then [D,{}] in the Rules of T by A2,XBOOLE_0:def 3;
then the InitialSym of T ==> <*> the carrier of T by A3;
then
A18: I ==> <*> the carrier of T by Th3;
A19: Terminals T = D by Th16;
thus Lang T c= D*
proof
let a be object;
assume a in Lang T;
then consider p being String of T such that
A20: a = p and
A21: rng p c= Terminals T and
p is_derivable_from <*the InitialSym of T*>;
p is FinSequence of D by A19,A21,FINSEQ_1:def 4;
hence thesis by A20,FINSEQ_1:def 11;
end;
let a be object;
assume
A22: a in D*;
then reconsider a as FinSequence of D by FINSEQ_1:def 11;
the carrier of T = succ D by Def10;
then rng a c= the carrier of T by A1;
then a is FinSequence of the carrier of T by FINSEQ_1:def 4;
then reconsider n = a as String of T by FINSEQ_1:def 11;
n^{} = n by FINSEQ_1:34;
then n^I ==> n by A18,Th5;
then
A23: n is_derivable_from n^I by Th7;
A24: X[0]
proof
let p be String of T;
assume len p = 0;
then p = {};
then p^I = I by FINSEQ_1:34;
hence thesis by Th6;
end;
A25: for k being Nat holds X[k] from NAT_1:sch 2(A24,A4);
len n = len n;
then n^I is_derivable_from I by A25,A22;
then
A26: n is_derivable_from I by A23,Th8;
rng a c= D;
hence thesis by A19,A26;
end;
definition
let IT be non empty GrammarStr;
attr IT is effective means
:Def11:
Lang IT is non empty & the InitialSym of
IT in NonTerminals IT & for s being Symbol of IT st s in Terminals IT ex p
being String of IT st p in Lang(IT) & s in rng p;
end;
definition
let IT be GrammarStr;
attr IT is finite means
the Rules of IT is finite;
end;
registration
cluster effective finite for non empty GrammarStr;
existence
proof
take G = EmptyGrammar 0;
A1: the Rules of G = {[0,{}]} by Def7;
the carrier of G = {0} by Def7;
then
A2: the InitialSym of G = 0 by TARSKI:def 1;
[0,{}] in {[0,{}]} by TARSKI:def 1;
then the InitialSym of G ==> <*> the carrier of G by A1,A2;
then
A3: the InitialSym of G in NonTerminals G;
A4: for s being Symbol of G st s in Terminals G ex p being String of G st p
in Lang(G) & s in rng p by Th10;
Lang(G) is non empty by Th11;
hence G is effective by A3,A4;
thus the Rules of G is finite by A1;
end;
end;
definition
let G be effective non empty GrammarStr;
redefine func NonTerminals G -> non empty Subset of G; :: redefines NonTerminals (LANG1, definition)
coherence
proof
NonTerminals G c= the carrier of G
proof
let a be object;
assume a in NonTerminals G;
then
ex s being Symbol of G st a = s & ex n being FinSequence st s ==> n;
hence thesis;
end;
hence thesis by Def11;
end;
end;
definition
let X,Y be non empty set, p be FinSequence of X, f be Function of X,Y;
redefine func f*p -> Element of Y*; :: redefines * (FUNCT_1, synonym) → * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
rng p c= X;
then reconsider g = p as Function of dom p, X by FUNCT_2:def 1,RELSET_1:4;
A1: rng (f*g) c= Y;
A2: dom p = Seg len p by FINSEQ_1:def 3;
dom (f*g) = dom p by FUNCT_2:def 1;
then f*g is FinSequence by A2,FINSEQ_1:def 2;
then f*g is FinSequence of Y by A1,FINSEQ_1:def 4;
hence thesis by FINSEQ_1:def 11;
end;
end;
definition
let X,Y be non empty set;
let f be Function of X,Y;
func f* -> Function of X*,Y* means
for p being Element of X* holds it.p = f* p;
existence
proof
deffunc U(Element of X*) = f*$1;
consider g being Function of X*,Y* such that
A1: for x being Element of X* holds g.x = U(x) from FUNCT_2:sch 4;
take g;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 be Function of X*,Y* such that
A2: for p being Element of X* holds f1.p = f*p and
A3: for p being Element of X* holds f2.p = f*p;
now
let x be Element of X*;
thus f1.x = f*x by A2
.= f2.x by A3;
end;
hence thesis by FUNCT_2:63;
end;
end;
reserve R for Relation,
x,y for set;
theorem
R c= R[*]
proof
let x,y be object;
A1: len <*x,y*> = 2 by FINSEQ_1:44;
A2: <*x,y*>.2 = y;
assume
A3: [x,y] in R;
then
A4: y in field R by RELAT_1:15;
A5: <*x,y*>.1 = x;
A6: now
let i be Nat such that
A7: i >= 1 and
A8: i < 2;
1+1 = 2;
then i <= 1 by A8,NAT_1:13;
then i = 1 by A7,XXREAL_0:1;
hence [<*x,y*>.i,<*x,y*>.(i+1)] in R by A3;
end;
x in field R by A3,RELAT_1:15;
hence thesis by A4,A1,A5,A2,A6,FINSEQ_1:def 17;
end;
definition
let X be non empty set, R be Relation of X;
redefine func R[*] -> Relation of X; :: redefines [*] (FINSEQ_1, definition)
coherence
proof
[:X,X:] c= [:X,X:];
then reconsider P = [:X,X:] as Relation of X;
R[*] c= P
proof
let x,y be object;
A1: field R c= X \/ X by RELSET_1:8;
assume
A2: [x,y] in R[*];
then
A3: y in field R by FINSEQ_1:def 17;
x in field R by A2,FINSEQ_1:def 17;
hence thesis by A3,A1,ZFMISC_1:87;
end;
hence thesis;
end;
end;
definition
let G be non empty GrammarStr;
let X be non empty set;
let f be Function of the carrier of G, X;
func G.f -> strict GrammarStr equals
GrammarStr (#X, f.the InitialSym of G,
(f)~*(the Rules of G)*(f*) #);
correctness;
end;
:: The goal is to show:
:: f is_one-to-one implies f*.:Lang(G) = Lang(G.f)