%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -*- Mode: Tex -*- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% pvs-gr.txt -- 
%% Author          : Sam Owre
%% Created On      : Thu Dec  2 13:45:18 1993
%% Last Modified By: Sam Owre
%% Last Modified On: Wed Nov  4 16:14:48 1998
%% Update Count    : 93
%% Status          : Unknown, Use with caution!
%% 
%% HISTORY
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Grammar PVS

Case Sensitive

Comment Character
	Newline  '%'

Operators
% Adding new operators may require modification to the following variables,
% and functions:
%  Var or Fun		File
%  ----------		----
%  *pvs-operators*	utils.lisp
%  
	'('  ')'  '-'  '+'  '*' '/' ':=' '|->'  ';'  ','  '='  '/='
	'<'  '<='  '>'  '>=' '{' '}' '[' ']' '.' '&' '<=>'
	'->' ':' '=>' '[#' '#]' '(#' '#)' '(:' ':)' '|'
        '^' '/\\' '\\/' '[]' '<>' '~' '==' '++' '**' '//' '^^'
	'<<' '>>' '::' '#' '@' '@@' '##' '[|' '|]' '|[' ']|' '!'
        '<<=' '>>=' '`' '\''
	'[||]' '||' '|-' '|=' '<|' '|>'

Lexical Terminals
	id, number, string %, literal

Precedence Information
  type-expr  '[' initial
             jux medial left

  expr  'HAS_TYPE' aggregate,
	'IN' aggregate % LET
	'|' medial left
	'|-' medial right, '|=' medial right
	'IFF' medial right, '<=>' medial right
	'IMPLIES' medial right, '=>' medial right, 'WHEN' medial right
	'OR' medial right, '\\/' medial right, 'XOR' medial right,
		'ORELSE' medial right
	'AND' medial right, '&' medial right, '/\\' medial right,
		'&&' medial right, 'ANDTHEN' medial right
	'NOT' initial, '~' initial
	'=' medial left, '/='  medial left, '==' medial left
		'<' medial left, '<=' medial left,
		'>' medial left, '>=' medial left,
		'<<' medial left, '>>' medial left,
                '<<=' medial left, '>>=' medial left,
		'<|' medial left, '|>' medial left
	'WITH' medial left
	'WHERE' medial left, 'IN' medial left
	'@' medial left, '#' medial left
	'@@' medial left, '##' medial left,
		'||' medial left
	'+' medial left, '-' medial left, '++' medial left, '~' medial left
	'*' medial left, '/' medial left, '**' medial left, '//' medial left
	'-' initial
	'O' medial left
	':' medial left, '::' medial left, 'HAS_TYPE' medial left
	'[]' initial, '<>' initial
	'^' medial left, '^^' medial left
	'`' medial left
	jux medial left  % application

adt-or-theories	::= {adt-or-theory+} <adt-or-modules(adt-or-theory+)>;

% SO - require endid so that multiple theories parse

adt-or-theory ::= {id [theory-formals] ':' {theory | datatype}}
		    <adt-or-module(id,[no-theory-formals()|theory-formals],
                                   alt)>;

theory ::= {'THEORY' [exporting]^e 'BEGIN' [assuming-part]^a
            [theory-part]^t 'END' id}
	      <module([noexp()|exporting]^e,
		      [noass()|assuming-part]^a,
                      [notheory()|theory-part]^t,id)>;

datatype ::= {'DATATYPE' ['WITH' 'SUBTYPES' {id^s ++ ','}]
	      'BEGIN' [{importing [';']^u}
                        <importing-elt(importing,[nosemic()|semic()]^u)>]^2
              [assuming-part]^1
	      adtcase+ 'END' id}
	        <[datatype(opt^1,opt^2,adtcases(plus),id)
		 |datatypes(subtypes(doubleplus),opt^1,opt^2,
                            adtcases(plus),id)]>;

adtcase ::= {constructor ':' idop [':' id]}
              <[adtcase(constructor,idop)
               |adtcase-subtype(constructor,idop,id)]>;

constructor ::= {idop [{'(' {{{idops ':' type-expr}
				<adtdecl(idops,type-expr)>} ++ ','} ')'}
			   <adtdecls(doubleplus)>]}
			<constructor(idop,opt)>;

theory-formals	::= {'[' {theory-formal ++ ','} ']'}
			<theory-formals(theory-formal+)>;

theory-formal ::= {[{'(' importing ')'}
                     <importing-elt(importing,nosemic())>]
                   idops ':' theory-formal-decl}
		     <theory-formal(opt,idops,theory-formal-decl)>;

theory-formal-decl ::= {type-keyword ['FROM' type-expr]}
		        <ftype-decl(type-keyword,[notype()|type-expr])>
		     | {type-expr} <fconst-decl(type-expr)>
		     ;

exporting ::= {'EXPORTING' exportings [{ 'WITH' exportingmods}]}
	        <exporting(exportings,[noexportingmods()|exportingmods])>;

exportings ::= {'ALL' ['BUT' {expname ++ ','}]}
			<exporting-all([noexpbuts()|expbuts(doubleplus)])>
		 |  {expname ++ ','}
			<expnames(doubleplus)>
		 ;

expname ::= {idop [':' {type-expr <type-expr> |
			'TYPE' <exptype()> |
			'FORMULA' <expformula()>}]}
			<expname(idop,[noexpkind()|alt])>
%		 |  {'|' idop '|'} <absexpname(idop)>
		 ;

exportingmods ::= 'ALL' <expmodall()>
		|  'CLOSURE' <expmodclosure()>
		|  modnames
		;

assuming-part ::= {'ASSUMING' assumings 'ENDASSUMING'} <assumings>;

assumings ::= {assuming+} <assuming-part(plus)>;

assuming ::= {importing [';']}
               <importing-elt(importing,[nosemic()|semic()])>
           | {judgement [';']}
                 <judgement-elt(judgement,[nosemic()|semic()])>
	   | {conversion [';']}
		 <conversion-elt(conversion,[nosemic()|semic()])>
	   | {idops pdformals* ':' assuming-decl [';']}
		<assuming(idops,pdf(star),assuming-decl,[nosemic()|semic()])>
	   ;

theory-part ::= {theory-elt+} <theory-part(plus)>;

theory-elt ::= {importing [';']}
                 <importing-elt(importing,[nosemic()|semic()])>
	     | {judgement [';']}
                 <judgement-elt(judgement,[nosemic()|semic()])>
	     | {conversion [';']}
		 <conversion-elt(conversion,[nosemic()|semic()])>
	     | {idops [pdformals+] ':' theory-decl [';']^s}
		 <theory(idops,[noformals()|pdf(plus)],
                         theory-decl,[nosemic()|semic()]^s)>
	     ;

importing ::= {'IMPORTING' {modname ++ ','}} <importing(modname+)>;

judgement ::= {'JUDGEMENT' {jdecl++','} {'HAS_TYPE'|'SUBTYPE_OF'} type-expr}
	      <{judgement(jdecls(doubleplus),
                 {has-type()|subtype-of()},type-expr)>;

jdecl ::= type-expr-sans-name <jsubtypedecl(type-expr-sans-name)>
        | number <jnumberdecl(number)>
        | {name [pdformals+]} <[jnamedecl(name)|jappldecl(name,pdf(plus))]>
        ;

ename ::= {name [':' type-expr]} <ename(name,[notype()|type-expr])>;

conversion ::= {'CONVERSION' {ename++','}} <conversion(ename+)>;

pdformals ::= {'(' adformals ')'} <adformals>;

adformals ::= {adformal++','} <adformals(adformal+)>;

adformal ::= typed-id
	   | {'(' typed-ids ')'} <typed-ids>
	   ;

assuming-decl ::= theory-decl | assumption;

theory-decl ::= lib-decl | mod-decl | type-decl | var-decl
              | const-decl | def-decl | ind-decl
              | formula-decl | datatype | judgement;

lib-decl ::= {'LIBRARY' ['='] string} <lib-decl([noeq()|eq()],string)>;

mod-decl ::= {'THEORY' '=' modname} <mod-decl(modname)>;

type-decl ::= {type-keyword [type-def ['CONTAINING' expr]^c]}
                <[uninterp-type-decl(type-keyword)
                 |type-decl(type-keyword,type-def,
                            [nocontains()|expr]^c)]>;

type-keyword ::= 'TYPE' <type()>
               | 'NONEMPTY_TYPE' <nonempty-type()>
               | 'TYPE+' <typeplus()>
               ;

% '=' must appear in name type-def, to avoid overlap with '=' as an opsym.
type-def ::= {{'=' <equal()> | 'FROM' <from()>} type-expr}
			<type-def(alt,type-expr)>;

var-decl ::= {'VAR' type-expr} <var-decl(type-expr)>;

const-decl ::= {type-expr [const-value]}
		<[uninterp-const-decl(type-expr)
		 |const-decl(type-expr,const-value)]>;

const-value ::= {'=' expr} <expr>;

def-decl ::= {'RECURSIVE' type-expr '=' expr 'MEASURE' expr^b ['BY' expr^r]}
		<def-decl(type-expr,expr,expr^b, [noexpr()| expr^r])>;

ind-decl ::= {'INDUCTIVE' type-expr '=' expr} <ind-decl(type-expr,expr)>;
		
assumption ::= {'ASSUMPTION' expr} <assumption(expr)>;

formula-decl ::= {formula-name expr} <formula-decl(formula-name,expr)>;

type-expr ::= {name [arguments]}
                <[type-name(name)|type-appl(name,arguments)]>
	    | type-expr-sans-name
	    ;

type-expr-sans-name ::= { '(' expr ')'} <expr-as-type(expr)>
		      | {'{' set-formals ['|' expr] '}'}
			<[enumtype(set-formals) | subtype(set-formals,expr)]>
		      | comp-type-expr
		      ;

% Broken out so that type expressions could appear in actual parameters;
% names cause conflicts.

comp-type-expr	::= recordtype
		 |  {[fun-array]^f '[' {dep-type-expr**','}
		     	[{'->' type-expr} <type-expr>]^r ']'}
		     <funtype(opt^f,dom(dep-type-expr*),opt^r)>
		 ;

recordtype ::= {'[#' {field-decls ++ ','} '#]'}
                <recordtype(fields(field-decls+))>;

field-decls ::= {ids ':' type-expr} <field-decls(ids,type-expr)>;

fun-array ::= 'FUNCTION' <function()> | 'ARRAY' <array()>;

dep-type-expr ::= type-expr
	       |  {idop ':' type-expr} <dep-binding(idop,type-expr)>
	       ;


%% Expressions

expr ::= number <number-expr(number)>
       | string <string-expr(string)>
       | name <name-expr(name)>
       | {'(:' {expr ** ','} ':)'} <list-expr(expr*)>
       | {'[|' {expr ** ','} '|]'} <brack-expr(expr*)>
       | {'(#' {assignment ++ ','} '#)'} <rec-expr(assignments(assignment+))>
       | {'(' {expr ** ','} ')'} <tuple-expr(expr*)>
       | {expr '`' {id | number}} <{fieldappl(expr,id)|projappl(expr,number)}>
       | {expr jux fun-arguments} <application(expr,fun-arguments)>
       | {expr 'O' expr^1} <term-expr(o(),expr-args(list(expr,expr^1)))>
       | {expr 'IFF' expr^1} <term-expr(iff(),expr-args(list(expr,expr^1)))>
       | {expr '<=>' expr^1} <term-expr(`\<=\>(),expr-args(list(expr,expr^1)))>
       | {expr 'IMPLIES' expr^1}
                    <term-expr(implies(),expr-args(list(expr,expr^1)))>
       | {expr '=>' expr^1} <term-expr(`=\>(),expr-args(list(expr,expr^1)))>
       | {expr 'WHEN' expr^1} <term-expr(when(),expr-args(list(expr,expr^1)))>
       | {expr 'OR' expr^1} <term-expr(or(),expr-args(list(expr,expr^1)))>
       | {expr '\\/' expr^1} <term-expr(`\\\/(),expr-args(list(expr,expr^1)))>
       | {expr 'AND' expr^1} <term-expr(and(),expr-args(list(expr,expr^1)))>
       | {expr '/\\' expr^1} <term-expr(`\/\\(),expr-args(list(expr,expr^1)))>
       | {expr '&' expr^1} <term-expr(`&(),expr-args(list(expr,expr^1)))>
       | {expr 'XOR' expr^1} <term-expr(xor(),expr-args(list(expr,expr^1)))>
       | {expr 'ANDTHEN' expr^1}
                    <term-expr(andthen(),expr-args(list(expr,expr^1)))>
       | {expr 'ORELSE' expr^1}
                    <term-expr(orelse(),expr-args(list(expr,expr^1)))>
       | {expr '^' expr^1} <term-expr(`^(),expr-args(list(expr,expr^1)))>
       | {expr '+' expr^1} <term-expr(`+(),expr-args(list(expr,expr^1)))>
       | {expr '-' expr^1} <term-expr(`-(),expr-args(list(expr,expr^1)))>
       | {expr '*' expr^1} <term-expr(`*(),expr-args(list(expr,expr^1)))>
       | {expr '/' expr^1} <term-expr(`\/(),expr-args(list(expr,expr^1)))>
       | {expr '++' expr^1} <term-expr(`++(),expr-args(list(expr,expr^1)))>
       | {expr '~' expr^1} <term-expr(`~(),expr-args(list(expr,expr^1)))>
       | {expr '**' expr^1} <term-expr(`**(),expr-args(list(expr,expr^1)))>
       | {expr '//' expr^1} <term-expr(`\/\/(),expr-args(list(expr,expr^1)))>
       | {expr '^^' expr^1} <term-expr(`\^\^(),expr-args(list(expr,expr^1)))>
       | {expr '|-' expr^1} <term-expr(`\|-(),expr-args(list(expr,expr^1)))>
       | {expr '|=' expr^1} <term-expr(`\|=(),expr-args(list(expr,expr^1)))>
       | {expr '<|' expr^1} <term-expr(`\<\|(),expr-args(list(expr,expr^1)))>
       | {expr '|>' expr^1} <term-expr(`\|\>(),expr-args(list(expr,expr^1)))>
       | {expr '=' expr^1} <term-expr(`=(),expr-args(list(expr,expr^1)))>
       | {expr '/=' expr^1} <term-expr(`\/=(),expr-args(list(expr,expr^1)))>
       | {expr '==' expr^1} <term-expr(`==(),expr-args(list(expr,expr^1)))>
       | {expr '<' expr^1} <term-expr(`\<(),expr-args(list(expr,expr^1)))>
       | {expr '<=' expr^1} <term-expr(`\<=(),expr-args(list(expr,expr^1)))>
       | {expr '>' expr^1} <term-expr(`\>(),expr-args(list(expr,expr^1)))>
       | {expr '>=' expr^1} <term-expr(`\>=(),expr-args(list(expr,expr^1)))>
       | {expr '<<' expr^1} <term-expr(`\<\<(),expr-args(list(expr,expr^1)))>
       | {expr '>>' expr^1} <term-expr(`\>\>(),expr-args(list(expr,expr^1)))>
       | {expr '<<=' expr^1} <term-expr(`\<\<=(),expr-args(list(expr,expr^1)))>
       | {expr '>>=' expr^1} <term-expr(`\>\>=(),expr-args(list(expr,expr^1)))>
       | {expr '#' expr^1} <term-expr(`#(),expr-args(list(expr,expr^1)))>
       | {expr '@@' expr^1} <term-expr(`\@\@(),expr-args(list(expr,expr^1)))>
       | {expr '##' expr^1} <term-expr(`\#\#(),expr-args(list(expr,expr^1)))>
       | {'NOT' expr} <unary-term-expr(not(),expr)>
       | {'~' expr} <unary-term-expr(`~(),expr)>
       | {'[]' expr} <unary-term-expr(`\[\](),expr)>
       | {'<>' expr} <unary-term-expr(`\<\>(),expr)>
       | {'-' expr} <unary-term-expr(`-(),expr)>
       | {expr '::' type-expr} <coercion(expr,type-coercion(type-expr))>
       | {'IF' expr^c 'THEN' expr^t
          {{'ELSIF' expr^ic 'THEN' expr^it} <elsif(expr^ic,expr^it)>}*
          'ELSE' expr^e 'ENDIF'}
          <if-expr(expr^c,expr^t,elsifs(star),expr^e)>
       | {{'LAMBDA' <lambda-expr()> | 'FORALL' <forall-expr()>
                                     | 'EXISTS' <exists-expr()>}
		     lambda-body}
	  <bind-expr(alt,lambda-body)>
       | {id '!' {number | lambda-body}^1}
	  <{skovar(id,number)| name-bind-expr(id,lambda-body)}^1>
       | set-expr
       | {'LET' {bind++','} 'IN' expr}
           <let-expr(let-bindings(doubleplus),expr)>
       | {expr 'WHERE' {bind++','}}
	  <where-expr(let-bindings(doubleplus),expr)>
       | {expr 'WITH' '[' {assignment ++ ','} ']'}
	  <update-expr(expr,assignments(assignment+))>
       | {'CASES' expr 'OF' {selection ++ ','}
		[{'ELSE' expr^e} <expr^e>] 'ENDCASES'}
	  <cases-expr(expr,args(selection+),opt)>
       | {'COND' {cond-case ++ ','}
		[{',' 'ELSE' '->' expr^e}] 'ENDCOND'}
	  <cond-expr(args(cond-case+),[noelse()|expr^e])>
       | table-expr
       ;

set-expr ::= {'{' set-formals '|' expr '}'} <set-expr(set-formals,expr)>;

cond-case ::= {expr^l '->' expr^r} <cond-case(expr^l,expr^r)>;

lambda-body ::= {lambda-formals ':' expr}
		   <lambda-body(lambda-formals,expr)>;

% What we would really like to say here is
%   lambda-formals ::= adformal++',' | pdformals+
% but this leads to problems: first, the adformals have optional ':'s,
% that can lead to ambiguities, second, the optional parens around the
% adformals clash with those around the pdformals.  Thus we make our own
% formals below.  Note that lambda-formals may be separated by a comma or
% not; an extra check is needed in parse.lisp to ensure it is being used
% correctly.

lambda-formals ::= {lambda-formal [[',']^c lambda-formals]}
			<[lambda-formal|
			  lambda-formals(lambda-formal,
					 [nocomma()|comma()]^c,
					 lambda-formals)]>;

lambda-formal ::= idop | pdformals ;

set-formals ::= {set-formal [[',']^c set-formals]}
		<[set-formal|
		  set-formals(set-formal,[nocomma()|comma()]^c,set-formals)]>;

%set-formals ::= {set-formal [set-formals-rest]}
%		<set-formals([no-set-formals()|set-formals-rest])>;
%
%set-formals-rest ::= {',' set-formal++','}
%			<set-formals-rest-commas(doubleplus)>
%		 |   {set-formal+}
%			<set-formals-rest(plus)>
%		 ;

set-formal ::= {{idop [':' type-expr]} | pdformals}
	       <{set-id(idop,[notype()|type-expr])|pdformals}>;

selection ::= {idop [{'(' idops ')'} <idops>] ':' expr}
	      <selection(idop,opt,expr)>;

% assignment	::= {expr {':='|'|->'} !+ @> expr^1 @^ !- }
%			<assignment(expr,expr^1,{ceq()|arr()})>;

assignment ::= {assign-arg+ {':='|'|->'} expr}
			<assignment(args(plus),expr,{ceq()|arr()})>;

assign-arg ::= {'(' expr++',' ')'} <assign-tuple(expr+)>
             | {'`' {id | number}} <{field-assign(id)|proj-assign(number)}>
	     | {id ['!' number]} <[assign-id(id)|assign-skoname(id,number)]>
             | number <assign-num(number)>
	     ;

table-expr ::= {'TABLE' [expr^1]^r [',' expr^2]^c [col-heading]^h
                 table-entries 'ENDTABLE'}
			<table-expr([norowvar()|expr^1]^r,
                                    [nocolvar()|expr^2]^c,
				    [nocolheading()|col-heading]^h,
				    table-entries)>;

col-heading ::= {'|[' expr^1 {'|' {expr | 'ELSE'}}+ ']|'}
		<col-heading(expr^1,colrest({expr|else()}+))>;

table-entries ::= {table-entry+} <table-entries(table-entry+)>;

table-entry ::= {{'|' [{expr | 'ELSE'}]}+ '||'}
			<table-entry([notableentry()|{expr|else()}]+)>;

bind ::= {{simplebind | {'(' simplebind++',' ')'}} '=' expr}
	 <bind({simplebind|binds(doubleplus)},expr)>;

simplebind ::= {idop pdformals* [':' type-expr]}
	       <simplebind(idop,pdf(star),[notype()|type-expr])>;

modnames ::= {modname ++ ','} <modnames(modname+)>;

modname ::= {[{id^1 '@'}]^p id [actuals] [mappings]^m}
	    <modname(id,[nolib()|id^1]^p,[noactuals()|actuals],
                        [nomap()|mappings]^m)>;

mappings ::= {'{' mapdecl++ ',' '}'} <mappings(mapdecl+)>;

mapdecl ::= {idops [pdformals+ <pdf(plus)>|theory-formals]
                   ':' {type-decl|const-decl} [';' <semic()>]^s}
	    <mapdecl(idops,opt,{type-decl|const-decl},opt^s)>;

names ::= {name ++ ','}	<names(name+)>;

fun-arguments ::= {'(' {expr ** ','} ')'} <fun-arguments(expr*)>;

arguments ::= {'(' {expr ++ ','} ')'} <arguments(expr+)>;

idops ::= {idop ++ ','} <idops(idop+)>;

idop ::=  id  <idop(id)> | opsym <idop(opsym)>;

ids ::= {id ++ ','} <ids(id+)>;

typed-id ::= {idop [':' type-expr]^t ['|' expr]^e} 
	     <typed-id(idop,[no-type-expr()|type-expr]^t,[no-pred()|expr]^e)>;

typed-ids ::= {idops [':' type-expr]^t ['|' expr]^e}
	      <{typed-ids(idops,[no-type-expr()|type-expr]^t,
				[no-pred()|expr]^e)>;

name ::= {[{id '@'}]^L idop [actuals] [{'.' idop^1}]^1}
	 <name(idop,[nolib()|id]^L,[noacts()|actuals],[nomod()|idop^1]^1)>;

unique-name ::= {name [':' {type-expr|formula-name}]}
		<unique-name
                  (name,[noqual()|{typed(type-expr)|formula(formula-name)}])>;

opsym ::= '+' <`+()> | '-' <`-()> | '*' <`*()> | '/' <`\/()>
	| '=' <`=()> | '/=' <`\/=()> | '==' <`==()> | '<' <`\<()>
	| '<=' <`\<=()> | '>' <`\>()> | '>=' <`\>=()>
	| 'IFF' <iff()> | 'IMPLIES' <implies()> | 'WHEN' <when()>
	| 'OR' <or()> | 'AND' <and()> | 'NOT' <not()> | '&' <`&()>
	| '/\\' <`\/\\()> | '\\/' <`\\\/()> | '^' <`^()>
	| '[]' <`\[\]()> | '<>' <`\<\>()> | '~' <`~()>
	| '=>' <`=\>()> | '<=>' <`\<=\>()> | 'IF' <if()>
	| 'TRUE' <true()> | 'FALSE' <false()> | 'O' <o()>
	| 'XOR' <xor()> | 'ORELSE' <orelse()> | 'ANDTHEN' <andthen()>
	| '++' <`++()> | '**' <`**()> | '//' <`\/\/()>
	| '^^' <`\^\^()> | '<<' <`\<\<()> | '>>' <`\>\>()>
        | '<<=' <`\<\<=()> | '>>=' <`\>\>=()>
	| '#' <`#()>
	| '@@' <`\@\@()> | '##' <`\#\#()>
	| '|-' <`\|-()> | '|=' <`\|=()> | '<|' <`\<\|()>
	| '|>' <`\|\>()> | '[||]' <`\[\|\|\]()>
	;

actuals ::= {'[' {actual ++ ','} ']'} <actuals(actual+)>;

actual ::= expr | comp-type-expr;

formula-name	::= 'AXIOM' <`AXIOM()> | 'CHALLENGE' <`CHALLENGE()>
		|   'CLAIM' <`CLAIM()> | 'CONJECTURE' <`CONJECTURE()>
		|   'COROLLARY' <`COROLLARY()> | 'FACT' <`FACT()>
		|   'FORMULA' <`FORMULA()> | 'LAW' <`LAW()>
                |   'LEMMA' <`LEMMA()> | 'OBLIGATION' <`OBLIGATION()>
		|   'POSTULATE' <`POSTULATE()>
		|   'PROPOSITION' <`PROPOSITION()> | 'SUBLEMMA' <`SUBLEMMA()>
		|   'THEOREM' <`THEOREM()>
		;