Constant Field Values

fmrisc.ProgramExplorer.*

fmrisc.ProgramExplorer.Main
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`copyright`	`"RISC ProgramExplorer Version 2.17 (July 4, 2017)\nhttp://www.risc.jku.at/research/formal/software/ProgramExplorer\n(C) 2008-, Research Institute for Symbolic Computation (RISC)\nThis is free software distributed under the terms of the GNU GPL.\nExecute \"ProgramExplorer -h\" to see the options available.\n------------------------------------------------------------------"`
`public static final java.lang.String`	`version`	`"2.17 (July 4, 2017)"`

fmrisc.ProgramExplorer.InOut.Directory
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`CONTEXT`	`"ProofNavigator"`
`public static final java.lang.String`	`FREED`	`"FREED"`
`public static final java.lang.String`	`taskdirname`	`".PETASKS"`

fmrisc.ProgramExplorer.InOut.Presenter
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`detailId`	`"detail"`
`public static final java.lang.String`	`detailName`	`"detail.xhtml"`
`public static final java.lang.String`	`detailName2`	`"detail-2.xhtml"`
`public static final java.lang.String`	`fileExt`	`".xhtml"`
`public static final java.lang.String`	`methodId`	`"method"`
`public static final java.lang.String`	`methodName`	`"method.xhtml"`
`public static final java.lang.String`	`nameFormStatAction`	`"formstat"`
`public static final java.lang.String`	`nameFormula`	`"formula"`
`public static final java.lang.String`	`nameMethod`	`"method"`
`public static final java.lang.String`	`namePrePost`	`"prepost"`
`public static final java.lang.String`	`nameStatement`	`"statement"`
`public static final java.lang.String`	`statPrefix`	`"stat"`
`public static final java.lang.String`	`statPrefix2`	`"stat-2"`

fmrisc.ProgramExplorer.Parser.MiniJavaLexer
Modifier and Type	Constant Field	Value
`public static final int`	`ANNOTATION`	`4`
`public static final int`	`CHAR`	`5`
`public static final int`	`DIGIT`	`6`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`7`
`public static final int`	`ESCAPED`	`8`
`public static final int`	`HEX`	`9`
`public static final int`	`IDENT`	`10`
`public static final int`	`INT`	`11`
`public static final int`	`LETTER`	`12`
`public static final int`	`REALLETTER`	`13`
`public static final int`	`STRING`	`14`
`public static final int`	`T__16`	`16`
`public static final int`	`T__17`	`17`
`public static final int`	`T__18`	`18`
`public static final int`	`T__19`	`19`
`public static final int`	`T__20`	`20`
`public static final int`	`T__21`	`21`
`public static final int`	`T__22`	`22`
`public static final int`	`T__23`	`23`
`public static final int`	`T__24`	`24`
`public static final int`	`T__25`	`25`
`public static final int`	`T__26`	`26`
`public static final int`	`T__27`	`27`
`public static final int`	`T__28`	`28`
`public static final int`	`T__29`	`29`
`public static final int`	`T__30`	`30`
`public static final int`	`T__31`	`31`
`public static final int`	`T__32`	`32`
`public static final int`	`T__33`	`33`
`public static final int`	`T__34`	`34`
`public static final int`	`T__35`	`35`
`public static final int`	`T__36`	`36`
`public static final int`	`T__37`	`37`
`public static final int`	`T__38`	`38`
`public static final int`	`T__39`	`39`
`public static final int`	`T__40`	`40`
`public static final int`	`T__41`	`41`
`public static final int`	`T__42`	`42`
`public static final int`	`T__43`	`43`
`public static final int`	`T__44`	`44`
`public static final int`	`T__45`	`45`
`public static final int`	`T__46`	`46`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`WS`	`15`

fmrisc.ProgramExplorer.Parser.MiniJavaParser
Modifier and Type	Constant Field	Value
`public static final int`	`ANNOTATION`	`4`
`public static final int`	`CHAR`	`5`
`public static final int`	`DIGIT`	`6`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`7`
`public static final int`	`ESCAPED`	`8`
`public static final int`	`HEX`	`9`
`public static final int`	`IDENT`	`10`
`public static final int`	`INT`	`11`
`public static final int`	`LETTER`	`12`
`public static final int`	`REALLETTER`	`13`
`public static final int`	`STRING`	`14`
`public static final int`	`T__16`	`16`
`public static final int`	`T__17`	`17`
`public static final int`	`T__18`	`18`
`public static final int`	`T__19`	`19`
`public static final int`	`T__20`	`20`
`public static final int`	`T__21`	`21`
`public static final int`	`T__22`	`22`
`public static final int`	`T__23`	`23`
`public static final int`	`T__24`	`24`
`public static final int`	`T__25`	`25`
`public static final int`	`T__26`	`26`
`public static final int`	`T__27`	`27`
`public static final int`	`T__28`	`28`
`public static final int`	`T__29`	`29`
`public static final int`	`T__30`	`30`
`public static final int`	`T__31`	`31`
`public static final int`	`T__32`	`32`
`public static final int`	`T__33`	`33`
`public static final int`	`T__34`	`34`
`public static final int`	`T__35`	`35`
`public static final int`	`T__36`	`36`
`public static final int`	`T__37`	`37`
`public static final int`	`T__38`	`38`
`public static final int`	`T__39`	`39`
`public static final int`	`T__40`	`40`
`public static final int`	`T__41`	`41`
`public static final int`	`T__42`	`42`
`public static final int`	`T__43`	`43`
`public static final int`	`T__44`	`44`
`public static final int`	`T__45`	`45`
`public static final int`	`T__46`	`46`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`WS`	`15`

fmrisc.ProgramExplorer.Parser.SpecLangLexer
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`41`
`public static final int`	`ASSIGNMENT`	`24`
`public static final int`	`ATSYMBOL`	`43`
`public static final int`	`BITAND`	`35`
`public static final int`	`BITNOT`	`37`
`public static final int`	`BITOR`	`36`
`public static final int`	`COLON`	`21`
`public static final int`	`COMMA`	`23`
`public static final int`	`COMMENT`	`44`
`public static final int`	`DIGIT`	`9`
`public static final int`	`DIVIDES`	`34`
`public static final int`	`DOTDOT`	`42`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`10`
`public static final int`	`EQUALITY`	`25`
`public static final int`	`EQUIV`	`40`
`public static final int`	`ESCAPED`	`11`
`public static final int`	`GREATER`	`29`
`public static final int`	`GREATEREQ`	`30`
`public static final int`	`HEX`	`46`
`public static final int`	`IDENT`	`4`
`public static final int`	`IMPLIES`	`39`
`public static final int`	`LBRACK`	`14`
`public static final int`	`LBRACKGRID`	`18`
`public static final int`	`LESS`	`27`
`public static final int`	`LESSEQ`	`28`
`public static final int`	`LETTER`	`8`
`public static final int`	`LPAR`	`12`
`public static final int`	`LPARGRID`	`16`
`public static final int`	`MINUS`	`32`
`public static final int`	`NONEQUALITY`	`26`
`public static final int`	`NUMBER`	`5`
`public static final int`	`PERIOD`	`20`
`public static final int`	`PLUS`	`31`
`public static final int`	`POWER`	`38`
`public static final int`	`RBRACK`	`15`
`public static final int`	`RBRACKGRID`	`19`
`public static final int`	`REALLETTER`	`7`
`public static final int`	`RPAR`	`13`
`public static final int`	`RPARGRID`	`17`
`public static final int`	`SEMICOLON`	`22`
`public static final int`	`STRING`	`6`
`public static final int`	`T__100`	`100`
`public static final int`	`T__101`	`101`
`public static final int`	`T__102`	`102`
`public static final int`	`T__103`	`103`
`public static final int`	`T__104`	`104`
`public static final int`	`T__105`	`105`
`public static final int`	`T__106`	`106`
`public static final int`	`T__107`	`107`
`public static final int`	`T__108`	`108`
`public static final int`	`T__109`	`109`
`public static final int`	`T__110`	`110`
`public static final int`	`T__111`	`111`
`public static final int`	`T__112`	`112`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`T__76`	`76`
`public static final int`	`T__77`	`77`
`public static final int`	`T__78`	`78`
`public static final int`	`T__79`	`79`
`public static final int`	`T__80`	`80`
`public static final int`	`T__81`	`81`
`public static final int`	`T__82`	`82`
`public static final int`	`T__83`	`83`
`public static final int`	`T__84`	`84`
`public static final int`	`T__85`	`85`
`public static final int`	`T__86`	`86`
`public static final int`	`T__87`	`87`
`public static final int`	`T__88`	`88`
`public static final int`	`T__89`	`89`
`public static final int`	`T__90`	`90`
`public static final int`	`T__91`	`91`
`public static final int`	`T__92`	`92`
`public static final int`	`T__93`	`93`
`public static final int`	`T__94`	`94`
`public static final int`	`T__95`	`95`
`public static final int`	`T__96`	`96`
`public static final int`	`T__97`	`97`
`public static final int`	`T__98`	`98`
`public static final int`	`T__99`	`99`
`public static final int`	`TIMES`	`33`
`public static final int`	`WS`	`45`

fmrisc.ProgramExplorer.Parser.SpecLangParser
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`41`
`public static final int`	`ASSIGNMENT`	`24`
`public static final int`	`ATSYMBOL`	`43`
`public static final int`	`BITAND`	`35`
`public static final int`	`BITNOT`	`37`
`public static final int`	`BITOR`	`36`
`public static final int`	`COLON`	`21`
`public static final int`	`COMMA`	`23`
`public static final int`	`COMMENT`	`44`
`public static final int`	`DIGIT`	`9`
`public static final int`	`DIVIDES`	`34`
`public static final int`	`DOTDOT`	`42`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`10`
`public static final int`	`EQUALITY`	`25`
`public static final int`	`EQUIV`	`40`
`public static final int`	`ESCAPED`	`11`
`public static final int`	`GREATER`	`29`
`public static final int`	`GREATEREQ`	`30`
`public static final int`	`HEX`	`46`
`public static final int`	`IDENT`	`4`
`public static final int`	`IMPLIES`	`39`
`public static final int`	`LBRACK`	`14`
`public static final int`	`LBRACKGRID`	`18`
`public static final int`	`LESS`	`27`
`public static final int`	`LESSEQ`	`28`
`public static final int`	`LETTER`	`8`
`public static final int`	`LPAR`	`12`
`public static final int`	`LPARGRID`	`16`
`public static final int`	`MINUS`	`32`
`public static final int`	`NONEQUALITY`	`26`
`public static final int`	`NUMBER`	`5`
`public static final int`	`PERIOD`	`20`
`public static final int`	`PLUS`	`31`
`public static final int`	`POWER`	`38`
`public static final int`	`RBRACK`	`15`
`public static final int`	`RBRACKGRID`	`19`
`public static final int`	`REALLETTER`	`7`
`public static final int`	`RPAR`	`13`
`public static final int`	`RPARGRID`	`17`
`public static final int`	`SEMICOLON`	`22`
`public static final int`	`STRING`	`6`
`public static final int`	`T__100`	`100`
`public static final int`	`T__101`	`101`
`public static final int`	`T__102`	`102`
`public static final int`	`T__103`	`103`
`public static final int`	`T__104`	`104`
`public static final int`	`T__105`	`105`
`public static final int`	`T__106`	`106`
`public static final int`	`T__107`	`107`
`public static final int`	`T__108`	`108`
`public static final int`	`T__109`	`109`
`public static final int`	`T__110`	`110`
`public static final int`	`T__111`	`111`
`public static final int`	`T__112`	`112`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`T__76`	`76`
`public static final int`	`T__77`	`77`
`public static final int`	`T__78`	`78`
`public static final int`	`T__79`	`79`
`public static final int`	`T__80`	`80`
`public static final int`	`T__81`	`81`
`public static final int`	`T__82`	`82`
`public static final int`	`T__83`	`83`
`public static final int`	`T__84`	`84`
`public static final int`	`T__85`	`85`
`public static final int`	`T__86`	`86`
`public static final int`	`T__87`	`87`
`public static final int`	`T__88`	`88`
`public static final int`	`T__89`	`89`
`public static final int`	`T__90`	`90`
`public static final int`	`T__91`	`91`
`public static final int`	`T__92`	`92`
`public static final int`	`T__93`	`93`
`public static final int`	`T__94`	`94`
`public static final int`	`T__95`	`95`
`public static final int`	`T__96`	`96`
`public static final int`	`T__97`	`97`
`public static final int`	`T__98`	`98`
`public static final int`	`T__99`	`99`
`public static final int`	`TIMES`	`33`
`public static final int`	`WS`	`45`

fmrisc.ProgramExplorer.Semantics.TypeTranslator
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`arrayLength`	`"length"`
`public static final java.lang.String`	`arrayValue`	`"value"`
`public static final java.lang.String`	`baseTheoryName`	`"Base"`
`public static final java.lang.String`	`charName`	`"char"`
`public static final java.lang.String`	`intDivName`	`"intDiv"`
`public static final java.lang.String`	`intDivName0`	`"intDiv0"`
`public static final java.lang.String`	`intDivOverflowName`	`"intDivOverflow"`
`public static final java.lang.String`	`intMinusName`	`"intMinus"`
`public static final java.lang.String`	`intMinusOverflowName`	`"intMinusOverflow"`
`public static final java.lang.String`	`intName`	`"int"`
`public static final java.lang.String`	`intNegName`	`"intNeg"`
`public static final java.lang.String`	`intNegOverflowName`	`"intNegOverflow"`
`public static final java.lang.String`	`intPlusName`	`"intPlus"`
`public static final java.lang.String`	`intPlusOverflowName`	`"intPlusOverflow"`
`public static final java.lang.String`	`intRemName`	`"intRem"`
`public static final java.lang.String`	`intTimesName`	`"intTimes"`
`public static final java.lang.String`	`intTimesOverflowName`	`"intTimesOverflow"`
`public static final java.lang.String`	`intTruncName`	`"intTrunc"`
`public static final java.lang.String`	`isNullName`	`"null"`
`public static final java.lang.String`	`maxIntName`	`"MAX_INT"`
`public static final java.lang.String`	`minIntName`	`"MIN_INT"`
`public static final java.lang.String`	`natName`	`"nat"`
`public static final java.lang.String`	`newArrayAxiomName`	`"newArrayAxiom"`
`public static final java.lang.String`	`newArrayName`	`"newArray"`
`public static final java.lang.String`	`newBooleanArrayAxiomName`	`"newBooleanArrayAxiom"`
`public static final java.lang.String`	`newBooleanArrayName`	`"newBooleanArray"`
`public static final java.lang.String`	`newCharArrayAxiomName`	`"newCharArrayAxiom"`
`public static final java.lang.String`	`newCharArrayName`	`"newCharArray"`
`public static final java.lang.String`	`newIntArrayAxiomName`	`"newIntArrayAxiom"`
`public static final java.lang.String`	`newIntArrayName`	`"newIntArray"`
`public static final java.lang.String`	`newName`	`"new"`
`public static final java.lang.String`	`newObjectName`	`"newObject"`
`public static final java.lang.String`	`newStringArrayAxiomName`	`"newStringArrayAxiom"`
`public static final java.lang.String`	`newStringArrayName`	`"newStringArray"`
`public static final java.lang.String`	`newStringName`	`"newString"`
`public static final java.lang.String`	`nullArrayName`	`"nullArray"`
`public static final java.lang.String`	`nullBooleanArrayName`	`"nullBooleanArray"`
`public static final java.lang.String`	`nullCharArrayName`	`"nullCharArray"`
`public static final java.lang.String`	`nullCharName`	`"nullChar"`
`public static final java.lang.String`	`nullIntArrayName`	`"nullIntArray"`
`public static final java.lang.String`	`nullName`	`"null"`
`public static final java.lang.String`	`nullStringArrayName`	`"nullStringArray"`
`public static final java.lang.String`	`nullStringName`	`"nullString"`
`public static final java.lang.String`	`typeArrayName`	`"Array"`
`public static final java.lang.String`	`typeBooleanArrayName`	`"BooleanArray"`
`public static final java.lang.String`	`typeCharArrayName`	`"CharArray"`
`public static final java.lang.String`	`typeIntArrayName`	`"IntArray"`
`public static final java.lang.String`	`typeStringArrayName`	`"StringArray"`
`public static final java.lang.String`	`zeroName`	`"zero"`

fmrisc.ProgramExplorer.SWT.MainSWT
Modifier and Type Constant Field Value

public static final java.lang.String riscImageName "risc-logo-transparent.png"

fmrisc.ProgramExplorer.SWT.MainSWT
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`riscImageName`	`"risc-logo-transparent.png"`

fmrisc.ProgramExplorer.SWT.TopWindow
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`helpURL`	`"http://www.risc.jku.at/research/formal/software/ProgramExplorer/manual"`
`public static final java.lang.String`	`helpURLOld`	`"http://www.risc.jku.at/research/formal/software/ProofNavigator/manual"`

fmrisc.ProgramExplorer.Syntax.Logic.AndFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "AND"

public static final int precedence 40

fmrisc.ProgramExplorer.Syntax.Logic.AndFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"AND"`
`public static final int`	`precedence`	`40`

fmrisc.ProgramExplorer.Syntax.Logic.ArrayType
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`arrayKeyword`	`"ARRAY"`
`public static final java.lang.String`	`baseKeyword`	`"OF"`

fmrisc.ProgramExplorer.Syntax.Logic.AtomicFormula
Modifier and Type Constant Field Value

public static final int precedence 70
fmrisc.ProgramExplorer.Syntax.Logic.AxiomDefinition
Modifier and Type Constant Field Value

public static final java.lang.String keyword "AXIOM"
fmrisc.ProgramExplorer.Syntax.Logic.BinaryAtomicFormula
Modifier and Type Constant Field Value

public static final int precedence 60
fmrisc.ProgramExplorer.Syntax.Logic.BitAndTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "&"

public static final int precedence 30
fmrisc.ProgramExplorer.Syntax.Logic.BitNegationTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "~"

public static final int precedence 50
fmrisc.ProgramExplorer.Syntax.Logic.BitOrTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "|"

public static final int precedence 20
fmrisc.ProgramExplorer.Syntax.Logic.DividesTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "/"

public static final int precedence 30
fmrisc.ProgramExplorer.Syntax.Logic.EqualsFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "="

fmrisc.ProgramExplorer.Syntax.Logic.AtomicFormula
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`70`

fmrisc.ProgramExplorer.Syntax.Logic.AxiomDefinition
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`keyword`	`"AXIOM"`

fmrisc.ProgramExplorer.Syntax.Logic.BinaryAtomicFormula
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`60`

fmrisc.ProgramExplorer.Syntax.Logic.BitAndTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"&"`
`public static final int`	`precedence`	`30`

fmrisc.ProgramExplorer.Syntax.Logic.BitNegationTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"~"`
`public static final int`	`precedence`	`50`

fmrisc.ProgramExplorer.Syntax.Logic.BitOrTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"\|"`
`public static final int`	`precedence`	`20`

fmrisc.ProgramExplorer.Syntax.Logic.EqualsFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"="`

fmrisc.ProgramExplorer.Syntax.Logic.EquivalentFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"<=>"`
`public static final int`	`precedence`	`20`

fmrisc.ProgramExplorer.Syntax.Logic.FormulaDefinition
Modifier and Type Constant Field Value

public static final java.lang.String keyword "FORMULA"
fmrisc.ProgramExplorer.Syntax.Logic.FunctionApplication
Modifier and Type Constant Field Value

public static final int precedence 80
fmrisc.ProgramExplorer.Syntax.Logic.GreaterEqualFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator ">="
fmrisc.ProgramExplorer.Syntax.Logic.GreaterFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator ">"

fmrisc.ProgramExplorer.Syntax.Logic.FormulaDefinition
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`keyword`	`"FORMULA"`

fmrisc.ProgramExplorer.Syntax.Logic.FunctionApplication
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`80`

fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`elseKeyword`	`"ELSE"`
`public static final java.lang.String`	`elsifKeyword`	`"ELSIF"`
`public static final java.lang.String`	`endifKeyword`	`"ENDIF"`
`public static final java.lang.String`	`ifKeyword`	`"IF"`
`public static final java.lang.String`	`thenKeyword`	`"THEN"`

fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseFormula
Modifier and Type Constant Field Value

public static final int precedence -1
fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
Modifier and Type Constant Field Value

public static final int precedence -1
fmrisc.ProgramExplorer.Syntax.Logic.ImpliesFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "=>"

public static final int precedence 20
fmrisc.ProgramExplorer.Syntax.Logic.LessEqualFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "<="
fmrisc.ProgramExplorer.Syntax.Logic.LessFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "<"

fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseFormula
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`-1`

fmrisc.ProgramExplorer.Syntax.Logic.IfThenElseTerm
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`-1`

fmrisc.ProgramExplorer.Syntax.Logic.ImpliesFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"=>"`
`public static final int`	`precedence`	`20`

fmrisc.ProgramExplorer.Syntax.Logic.LessFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"<"`

fmrisc.ProgramExplorer.Syntax.Logic.LetExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`inKeyword`	`"IN"`
`public static final java.lang.String`	`letKeyword`	`"LET"`
`public static final int`	`precedence`	`10`

fmrisc.ProgramExplorer.Syntax.Logic.MinusTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "-"

public static final int precedence 20
fmrisc.ProgramExplorer.Syntax.Logic.NegationTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "-"

public static final int precedence 50
fmrisc.ProgramExplorer.Syntax.Logic.NewState
Modifier and Type Constant Field Value

public static final java.lang.String newStateKeyword "NEXT"
fmrisc.ProgramExplorer.Syntax.Logic.NotEqualsFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "/="

fmrisc.ProgramExplorer.Syntax.Logic.NewState
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`newStateKeyword`	`"NEXT"`

fmrisc.ProgramExplorer.Syntax.Logic.NotEqualsFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"/="`

fmrisc.ProgramExplorer.Syntax.Logic.NotEquivalentFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"XOR"`
`public static final int`	`precedence`	`20`

fmrisc.ProgramExplorer.Syntax.Logic.NotFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "NOT"

public static final int precedence 50
fmrisc.ProgramExplorer.Syntax.Logic.OldState
Modifier and Type Constant Field Value

public static final java.lang.String oldStateKeyword "NOW"
fmrisc.ProgramExplorer.Syntax.Logic.OrFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "OR"

public static final int precedence 30
fmrisc.ProgramExplorer.Syntax.Logic.PlusTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "+"

public static final int precedence 20
fmrisc.ProgramExplorer.Syntax.Logic.PostfixApplication
Modifier and Type Constant Field Value

public static final java.lang.String operator "@"
fmrisc.ProgramExplorer.Syntax.Logic.PostfixFormula
Modifier and Type Constant Field Value

public static final int precedence 70
fmrisc.ProgramExplorer.Syntax.Logic.PostVariable
Modifier and Type Constant Field Value

public static final java.lang.String keyword "VAR"
fmrisc.ProgramExplorer.Syntax.Logic.PowerTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "^"

public static final int precedence 40
fmrisc.ProgramExplorer.Syntax.Logic.PreVariable
Modifier and Type Constant Field Value

public static final java.lang.String keyword "OLD"
fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariableBase
Modifier and Type Constant Field Value

public static final int precedence 148
fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
Modifier and Type Constant Field Value

public static final int precedence 0
fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedTerm
Modifier and Type Constant Field Value

public static final int precedence 10

fmrisc.ProgramExplorer.Syntax.Logic.NotFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"NOT"`
`public static final int`	`precedence`	`50`

fmrisc.ProgramExplorer.Syntax.Logic.OldState
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`oldStateKeyword`	`"NOW"`

fmrisc.ProgramExplorer.Syntax.Logic.OrFormula
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"OR"`
`public static final int`	`precedence`	`30`

fmrisc.ProgramExplorer.Syntax.Logic.PostfixApplication
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"@"`

fmrisc.ProgramExplorer.Syntax.Logic.PostfixFormula
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`70`

fmrisc.ProgramExplorer.Syntax.Logic.PostVariable
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`keyword`	`"VAR"`

fmrisc.ProgramExplorer.Syntax.Logic.PowerTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"^"`
`public static final int`	`precedence`	`40`

fmrisc.ProgramExplorer.Syntax.Logic.PreVariable
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`keyword`	`"OLD"`

fmrisc.ProgramExplorer.Syntax.Logic.ProgramVariableBase
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`148`

fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedExpression
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`0`

fmrisc.ProgramExplorer.Syntax.Logic.QuantifiedTerm
Modifier and Type	Constant Field	Value
`public static final int`	`precedence`	`10`

fmrisc.ProgramExplorer.Syntax.Logic.RecordTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`beginToken`	`"(#"`
`public static final java.lang.String`	`endToken`	`"#)"`

fmrisc.ProgramExplorer.Syntax.Logic.RecordType
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`beginToken`	`"[#"`
`public static final java.lang.String`	`endToken`	`"#]"`

fmrisc.ProgramExplorer.Syntax.Logic.SimilarFormula
Modifier and Type Constant Field Value

public static final java.lang.String operator "~"
fmrisc.ProgramExplorer.Syntax.Logic.StateType
Modifier and Type Constant Field Value

public static final java.lang.String stateKeyword "STATE"
fmrisc.ProgramExplorer.Syntax.Logic.StringType
Modifier and Type Constant Field Value

public static final java.lang.String stringKeyword "STRING"

fmrisc.ProgramExplorer.Syntax.Logic.SubrangeType
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`beginToken`	`"["`
`public static final java.lang.String`	`endToken`	`"]"`
`public static final java.lang.String`	`separatorToken`	`".."`

fmrisc.ProgramExplorer.Syntax.Logic.SubType
Modifier and Type Constant Field Value

public static final java.lang.String keyword "SUBTYPE"
fmrisc.ProgramExplorer.Syntax.Logic.TimesTerm
Modifier and Type Constant Field Value

public static final java.lang.String operator "*"

public static final int precedence 30

fmrisc.ProgramExplorer.Syntax.Logic.TupleTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`beginToken`	`"("`
`public static final java.lang.String`	`endToken`	`")"`

fmrisc.ProgramExplorer.Syntax.Logic.TupleType
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`beginToken`	`"["`
`public static final java.lang.String`	`endToken`	`"]"`

fmrisc.ProgramExplorer.Syntax.Logic.TypeDeclaration
Modifier and Type Constant Field Value

public static final java.lang.String keyword "TYPE"

fmrisc.ProgramExplorer.Syntax.Logic.UpdateTerm
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`assignToken`	`":="`
`public static final java.lang.String`	`withKeyword`	`"WITH"`

fmrisc.ProgramExplorer.Syntax.Program.AndExpression
Modifier and Type Constant Field Value

public static final java.lang.String operator "&&"

public static final int precedence 4
fmrisc.ProgramExplorer.Syntax.Program.BooleanLiteral
Modifier and Type Constant Field Value

public static final int precedence 16
fmrisc.ProgramExplorer.Syntax.Program.CharLiteral
Modifier and Type Constant Field Value

public static final int precedence 16

fmrisc.ProgramExplorer.Syntax.Program.DividesExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"/"`
`public static final int`	`precedence`	`12`

fmrisc.ProgramExplorer.Syntax.Program.EqualsExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"=="`
`public static final int`	`precedence`	`8`

fmrisc.ProgramExplorer.Syntax.Program.GreaterEqualExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`">="`
`public static final int`	`precedence`	`9`

fmrisc.ProgramExplorer.Syntax.Program.GreaterExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`">"`
`public static final int`	`precedence`	`9`

fmrisc.ProgramExplorer.Syntax.Program.IntLiteral
Modifier and Type Constant Field Value

public static final int precedence 16
fmrisc.ProgramExplorer.Syntax.Program.IntType
Modifier and Type Constant Field Value

public final int max 2147483647

public final int min -2147483648

fmrisc.ProgramExplorer.Syntax.Program.LessEqualExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"<="`
`public static final int`	`precedence`	`9`

fmrisc.ProgramExplorer.Syntax.Program.LessExpression
Modifier and Type Constant Field Value

public static final java.lang.String operator "<"

public static final int precedence 9

fmrisc.ProgramExplorer.Syntax.Program.MinusExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"-"`
`public static final int`	`precedence`	`11`

fmrisc.ProgramExplorer.Syntax.Program.NegationExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"-"`
`public static final int`	`precedence`	`14`

fmrisc.ProgramExplorer.Syntax.Program.NewArrayExpression
Modifier and Type Constant Field Value

public static final int precedence 13

fmrisc.ProgramExplorer.Syntax.Program.NotEqualsExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"!="`
`public static final int`	`precedence`	`8`

fmrisc.ProgramExplorer.Syntax.Program.NotExpression
Modifier and Type Constant Field Value

public static final java.lang.String operator "!"

public static final int precedence 14
fmrisc.ProgramExplorer.Syntax.Program.NullLiteral
Modifier and Type Constant Field Value

public static final int precedence 16
fmrisc.ProgramExplorer.Syntax.Program.OrExpression
Modifier and Type Constant Field Value

public static final java.lang.String operator "||"

public static final int precedence 3

fmrisc.ProgramExplorer.Syntax.Program.PercentExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"%"`
`public static final int`	`precedence`	`12`

fmrisc.ProgramExplorer.Syntax.Program.PlusExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"+"`
`public static final int`	`precedence`	`11`

fmrisc.ProgramExplorer.Syntax.Program.SelectorExpression
Modifier and Type Constant Field Value

public static final int precedence 15
fmrisc.ProgramExplorer.Syntax.Program.StringLiteral
Modifier and Type Constant Field Value

public static final int precedence 16
fmrisc.ProgramExplorer.Syntax.Program.StringType
Modifier and Type Constant Field Value

public static final java.lang.String name "String"

fmrisc.ProgramExplorer.Syntax.Program.TimesExpression
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"*"`
`public static final int`	`precedence`	`12`

fmrisc.ProgramExplorer.Syntax.Program.VariableValue
Modifier and Type Constant Field Value

public static final int precedence 16

fmrisc.ProgramExplorer.Syntax.Spec.ClassSpec
Modifier and Type Constant Field Value

public static final java.lang.String invariantKeyword "invariant"

fmrisc.ProgramExplorer.Syntax.Spec.LoopSpec
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`invariantKeyword`	`"invariant"`
`public static final java.lang.String`	`terminationKeyword`	`"decreases"`

fmrisc.ProgramExplorer.Syntax.Spec.MethodSpec
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`divergesKeyword`	`"diverges"`
`public static final java.lang.String`	`exceptionsKeyword`	`"signals"`
`public static final java.lang.String`	`postKeyword`	`"ensures"`
`public static final java.lang.String`	`preKeyword`	`"requires"`
`public static final java.lang.String`	`terminationKeyword`	`"decreases"`
`public static final java.lang.String`	`variablesKeyword`	`"assignable"`

fmrisc.ProgramExplorer.Syntax.Spec.StatementSpec
Modifier and Type Constant Field Value

public static final java.lang.String assertionKeyword "assert"

fmrisc.ProgramExplorer.Tasks.TerminationTasks
Modifier and Type Constant Field Value

public static final boolean avoidTasks true

fmrisc.ProofNavigator.*

fmrisc.ProofNavigator.PN2Lexer
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`38`
`public static final int`	`ASSIGNMENT`	`24`
`public static final int`	`COLON`	`22`
`public static final int`	`COMMA`	`23`
`public static final int`	`COMMENT`	`41`
`public static final int`	`DIGIT`	`12`
`public static final int`	`DIVIDES`	`34`
`public static final int`	`DOTDOT`	`39`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`40`
`public static final int`	`EQUALITY`	`25`
`public static final int`	`EQUIV`	`37`
`public static final int`	`GREATER`	`29`
`public static final int`	`GREATEREQ`	`30`
`public static final int`	`IDENT`	`5`
`public static final int`	`IMPLIES`	`36`
`public static final int`	`LABEL`	`6`
`public static final int`	`LBRACK`	`15`
`public static final int`	`LBRACKGRID`	`19`
`public static final int`	`LESS`	`27`
`public static final int`	`LESSEQ`	`28`
`public static final int`	`LETTER`	`11`
`public static final int`	`LPAR`	`13`
`public static final int`	`LPARGRID`	`17`
`public static final int`	`MINUS`	`32`
`public static final int`	`NONEQUALITY`	`26`
`public static final int`	`NUMBER`	`8`
`public static final int`	`PERIOD`	`21`
`public static final int`	`PLUS`	`31`
`public static final int`	`POWER`	`35`
`public static final int`	`RBRACK`	`16`
`public static final int`	`RBRACKGRID`	`20`
`public static final int`	`REALLETTER`	`10`
`public static final int`	`RPAR`	`14`
`public static final int`	`RPARGRID`	`18`
`public static final int`	`SEMICOLON`	`4`
`public static final int`	`STRING`	`7`
`public static final int`	`T__100`	`100`
`public static final int`	`T__101`	`101`
`public static final int`	`T__102`	`102`
`public static final int`	`T__103`	`103`
`public static final int`	`T__104`	`104`
`public static final int`	`T__105`	`105`
`public static final int`	`T__106`	`106`
`public static final int`	`T__43`	`43`
`public static final int`	`T__44`	`44`
`public static final int`	`T__45`	`45`
`public static final int`	`T__46`	`46`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`T__76`	`76`
`public static final int`	`T__77`	`77`
`public static final int`	`T__78`	`78`
`public static final int`	`T__79`	`79`
`public static final int`	`T__80`	`80`
`public static final int`	`T__81`	`81`
`public static final int`	`T__82`	`82`
`public static final int`	`T__83`	`83`
`public static final int`	`T__84`	`84`
`public static final int`	`T__85`	`85`
`public static final int`	`T__86`	`86`
`public static final int`	`T__87`	`87`
`public static final int`	`T__88`	`88`
`public static final int`	`T__89`	`89`
`public static final int`	`T__90`	`90`
`public static final int`	`T__91`	`91`
`public static final int`	`T__92`	`92`
`public static final int`	`T__93`	`93`
`public static final int`	`T__94`	`94`
`public static final int`	`T__95`	`95`
`public static final int`	`T__96`	`96`
`public static final int`	`T__97`	`97`
`public static final int`	`T__98`	`98`
`public static final int`	`T__99`	`99`
`public static final int`	`TIMES`	`33`
`public static final int`	`UNDERSCORE`	`9`
`public static final int`	`WS`	`42`

fmrisc.ProofNavigator.PN2Parser
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`38`
`public static final int`	`ASSIGNMENT`	`24`
`public static final int`	`COLON`	`22`
`public static final int`	`COMMA`	`23`
`public static final int`	`COMMENT`	`41`
`public static final int`	`DIGIT`	`12`
`public static final int`	`DIVIDES`	`34`
`public static final int`	`DOTDOT`	`39`
`public static final int`	`EOF`	`-1`
`public static final int`	`EOL`	`40`
`public static final int`	`EQUALITY`	`25`
`public static final int`	`EQUIV`	`37`
`public static final int`	`GREATER`	`29`
`public static final int`	`GREATEREQ`	`30`
`public static final int`	`IDENT`	`5`
`public static final int`	`IMPLIES`	`36`
`public static final int`	`LABEL`	`6`
`public static final int`	`LBRACK`	`15`
`public static final int`	`LBRACKGRID`	`19`
`public static final int`	`LESS`	`27`
`public static final int`	`LESSEQ`	`28`
`public static final int`	`LETTER`	`11`
`public static final int`	`LPAR`	`13`
`public static final int`	`LPARGRID`	`17`
`public static final int`	`MINUS`	`32`
`public static final int`	`NONEQUALITY`	`26`
`public static final int`	`NUMBER`	`8`
`public static final int`	`PERIOD`	`21`
`public static final int`	`PLUS`	`31`
`public static final int`	`POWER`	`35`
`public static final int`	`RBRACK`	`16`
`public static final int`	`RBRACKGRID`	`20`
`public static final int`	`REALLETTER`	`10`
`public static final int`	`RPAR`	`14`
`public static final int`	`RPARGRID`	`18`
`public static final int`	`SEMICOLON`	`4`
`public static final int`	`STRING`	`7`
`public static final int`	`T__100`	`100`
`public static final int`	`T__101`	`101`
`public static final int`	`T__102`	`102`
`public static final int`	`T__103`	`103`
`public static final int`	`T__104`	`104`
`public static final int`	`T__105`	`105`
`public static final int`	`T__106`	`106`
`public static final int`	`T__43`	`43`
`public static final int`	`T__44`	`44`
`public static final int`	`T__45`	`45`
`public static final int`	`T__46`	`46`
`public static final int`	`T__47`	`47`
`public static final int`	`T__48`	`48`
`public static final int`	`T__49`	`49`
`public static final int`	`T__50`	`50`
`public static final int`	`T__51`	`51`
`public static final int`	`T__52`	`52`
`public static final int`	`T__53`	`53`
`public static final int`	`T__54`	`54`
`public static final int`	`T__55`	`55`
`public static final int`	`T__56`	`56`
`public static final int`	`T__57`	`57`
`public static final int`	`T__58`	`58`
`public static final int`	`T__59`	`59`
`public static final int`	`T__60`	`60`
`public static final int`	`T__61`	`61`
`public static final int`	`T__62`	`62`
`public static final int`	`T__63`	`63`
`public static final int`	`T__64`	`64`
`public static final int`	`T__65`	`65`
`public static final int`	`T__66`	`66`
`public static final int`	`T__67`	`67`
`public static final int`	`T__68`	`68`
`public static final int`	`T__69`	`69`
`public static final int`	`T__70`	`70`
`public static final int`	`T__71`	`71`
`public static final int`	`T__72`	`72`
`public static final int`	`T__73`	`73`
`public static final int`	`T__74`	`74`
`public static final int`	`T__75`	`75`
`public static final int`	`T__76`	`76`
`public static final int`	`T__77`	`77`
`public static final int`	`T__78`	`78`
`public static final int`	`T__79`	`79`
`public static final int`	`T__80`	`80`
`public static final int`	`T__81`	`81`
`public static final int`	`T__82`	`82`
`public static final int`	`T__83`	`83`
`public static final int`	`T__84`	`84`
`public static final int`	`T__85`	`85`
`public static final int`	`T__86`	`86`
`public static final int`	`T__87`	`87`
`public static final int`	`T__88`	`88`
`public static final int`	`T__89`	`89`
`public static final int`	`T__90`	`90`
`public static final int`	`T__91`	`91`
`public static final int`	`T__92`	`92`
`public static final int`	`T__93`	`93`
`public static final int`	`T__94`	`94`
`public static final int`	`T__95`	`95`
`public static final int`	`T__96`	`96`
`public static final int`	`T__97`	`97`
`public static final int`	`T__98`	`98`
`public static final int`	`T__99`	`99`
`public static final int`	`TIMES`	`33`
`public static final int`	`UNDERSCORE`	`9`
`public static final int`	`WS`	`42`

fmrisc.ProofNavigator.PNParserTokenTypes
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`139`
`public static final int`	`ASSIGNMENT`	`122`
`public static final int`	`BITAND`	`134`
`public static final int`	`BITNOT`	`136`
`public static final int`	`BITOR`	`131`
`public static final int`	`COLON`	`120`
`public static final int`	`COMMA`	`121`
`public static final int`	`COMMENT`	`146`
`public static final int`	`DIGIT`	`143`
`public static final int`	`DIVIDES`	`133`
`public static final int`	`DOTDOT`	`140`
`public static final int`	`EOF`	`1`
`public static final int`	`EOL`	`145`
`public static final int`	`EQUALITY`	`123`
`public static final int`	`EQUIV`	`138`
`public static final int`	`GREATER`	`127`
`public static final int`	`GREATEREQ`	`128`
`public static final int`	`IDENT`	`7`
`public static final int`	`IGNORE`	`110`
`public static final int`	`IMPLIES`	`137`
`public static final int`	`LABEL`	`9`
`public static final int`	`LBRACK`	`113`
`public static final int`	`LBRACKGRID`	`117`
`public static final int`	`LESS`	`125`
`public static final int`	`LESSEQ`	`126`
`public static final int`	`LETTER`	`142`
`public static final int`	`LITERAL_AND`	`77`
`public static final int`	`LITERAL_ARRAY`	`54`
`public static final int`	`LITERAL_assume`	`21`
`public static final int`	`LITERAL_auto`	`17`
`public static final int`	`LITERAL_autostar`	`19`
`public static final int`	`LITERAL_AXIOM`	`50`
`public static final int`	`LITERAL_BIT`	`57`
`public static final int`	`LITERAL_BITFALSE`	`102`
`public static final int`	`LITERAL_BITTRUE`	`101`
`public static final int`	`LITERAL_BOOLEAN`	`56`
`public static final int`	`LITERAL_case`	`22`
`public static final int`	`LITERAL_counterexample`	`20`
`public static final int`	`LITERAL_decompose`	`15`
`public static final int`	`LITERAL_ELSE`	`108`
`public static final int`	`LITERAL_ELSIF`	`107`
`public static final int`	`LITERAL_ENDIF`	`109`
`public static final int`	`LITERAL_environment`	`35`
`public static final int`	`LITERAL_EXISTS`	`70`
`public static final int`	`LITERAL_expand`	`27`
`public static final int`	`LITERAL_FALSE`	`98`
`public static final int`	`LITERAL_flatten`	`12`
`public static final int`	`LITERAL_flip`	`8`
`public static final int`	`LITERAL_FORALL`	`69`
`public static final int`	`LITERAL_FORMULA`	`49`
`public static final int`	`LITERAL_goal`	`10`
`public static final int`	`LITERAL_goto`	`32`
`public static final int`	`LITERAL_IF`	`105`
`public static final int`	`LITERAL_in`	`25`
`public static final int`	`LITERAL_IN`	`72`
`public static final int`	`LITERAL_induction`	`28`
`public static final int`	`LITERAL_instantiate`	`24`
`public static final int`	`LITERAL_INT`	`59`
`public static final int`	`LITERAL_LAMBDA`	`68`
`public static final int`	`LITERAL_lemma`	`23`
`public static final int`	`LITERAL_LET`	`71`
`public static final int`	`LITERAL_LOGICAL`	`58`
`public static final int`	`LITERAL_LOGICALFALSE`	`100`
`public static final int`	`LITERAL_LOGICALTRUE`	`99`
`public static final int`	`LITERAL_NAT`	`60`
`public static final int`	`LITERAL_newcontext`	`46`
`public static final int`	`LITERAL_next`	`30`
`public static final int`	`LITERAL_NOT`	`78`
`public static final int`	`LITERAL_OF`	`55`
`public static final int`	`LITERAL_open`	`29`
`public static final int`	`LITERAL_option`	`44`
`public static final int`	`LITERAL_OR`	`76`
`public static final int`	`LITERAL_prev`	`31`
`public static final int`	`LITERAL_printf`	`40`
`public static final int`	`LITERAL_printt`	`38`
`public static final int`	`LITERAL_printv`	`39`
`public static final int`	`LITERAL_proof`	`36`
`public static final int`	`LITERAL_prove`	`6`
`public static final int`	`LITERAL_quit`	`41`
`public static final int`	`LITERAL_read`	`42`
`public static final int`	`LITERAL_REAL`	`61`
`public static final int`	`LITERAL_redo`	`34`
`public static final int`	`LITERAL_scatter`	`16`
`public static final int`	`LITERAL_simplify`	`14`
`public static final int`	`LITERAL_skolemize`	`11`
`public static final int`	`LITERAL_split`	`13`
`public static final int`	`LITERAL_state`	`37`
`public static final int`	`LITERAL_SUBTYPE`	`66`
`public static final int`	`LITERAL_tcc`	`5`
`public static final int`	`LITERAL_THEN`	`106`
`public static final int`	`LITERAL_TRUE`	`97`
`public static final int`	`LITERAL_TYPE`	`48`
`public static final int`	`LITERAL_typeaxiom`	`26`
`public static final int`	`LITERAL_undo`	`33`
`public static final int`	`LITERAL_WITH`	`92`
`public static final int`	`LITERAL_XOR`	`75`
`public static final int`	`LPAR`	`111`
`public static final int`	`LPARGRID`	`115`
`public static final int`	`MINUS`	`130`
`public static final int`	`NONEQUALITY`	`124`
`public static final int`	`NULL_TREE_LOOKAHEAD`	`3`
`public static final int`	`NUMBER`	`94`
`public static final int`	`PERIOD`	`119`
`public static final int`	`PLUS`	`129`
`public static final int`	`POWER`	`135`
`public static final int`	`RBRACK`	`114`
`public static final int`	`RBRACKGRID`	`118`
`public static final int`	`REALLETTER`	`141`
`public static final int`	`RPAR`	`112`
`public static final int`	`RPARGRID`	`116`
`public static final int`	`SEMICOLON`	`4`
`public static final int`	`STRING`	`43`
`public static final int`	`TIMES`	`132`
`public static final int`	`UNDERSCORE`	`96`
`public static final int`	`WS`	`144`

fmrisc.ProofNavigator.State
Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`NamespacePrefix`	`"fmrisc"`
`public static final java.lang.String`	`NamespaceURI`	`"http://www.risc.uni-linz.ac.at/FM-RISC"`
`public static final java.lang.String`	`OMDocPrefix`	`"omdoc"`
`public static final java.lang.String`	`OMDocURI`	`"http://www.mathweb.org/omdoc"`
`public static final java.lang.String`	`OpenMathPrefix`	`"om"`
`public static final java.lang.String`	`OpenMathURI`	`"http://www.openmath.org/OpenMath"`
`public static final java.lang.String`	`XMLPrefix`	`"xml"`
`public static final java.lang.String`	`XMLURI`	`"http://www.w3.org/XML/1998/namespace"`

fmrisc.ProofNavigator.Commands.Assume
Modifier and Type Constant Field Value

public static final java.lang.String Name "assume"
fmrisc.ProofNavigator.Commands.Auto
Modifier and Type Constant Field Value

public static final java.lang.String Name "auto"
fmrisc.ProofNavigator.Commands.AutoStar
Modifier and Type Constant Field Value

public static final java.lang.String Name "autostar"
fmrisc.ProofNavigator.Commands.Case
Modifier and Type Constant Field Value

public static final java.lang.String Name "case"
fmrisc.ProofNavigator.Commands.ContextC
Modifier and Type Constant Field Value

public static final java.lang.String Name "newcontext"
fmrisc.ProofNavigator.Commands.CounterExample
Modifier and Type Constant Field Value

public static final java.lang.String Name "counterexample"
fmrisc.ProofNavigator.Commands.DeclarationC
Modifier and Type Constant Field Value

public static final java.lang.String Name "declaration"
fmrisc.ProofNavigator.Commands.Decompose
Modifier and Type Constant Field Value

public static final java.lang.String Name "decompose"
fmrisc.ProofNavigator.Commands.Empty
Modifier and Type Constant Field Value

public static final java.lang.String Name "empty"
fmrisc.ProofNavigator.Commands.EnvironmentC
Modifier and Type Constant Field Value

public static final java.lang.String Name "environment"
fmrisc.ProofNavigator.Commands.Expand
Modifier and Type Constant Field Value

public static final java.lang.String Name "expand"
fmrisc.ProofNavigator.Commands.Flatten
Modifier and Type Constant Field Value

public static final java.lang.String Name "flatten"
fmrisc.ProofNavigator.Commands.Flip
Modifier and Type Constant Field Value

public static final java.lang.String Name "flip"
fmrisc.ProofNavigator.Commands.FormulaC
Modifier and Type Constant Field Value

public static final java.lang.String Name "printf"
fmrisc.ProofNavigator.Commands.Goal
Modifier and Type Constant Field Value

public static final java.lang.String Name "goal"
fmrisc.ProofNavigator.Commands.Goto
Modifier and Type Constant Field Value

public static final java.lang.String Name "goto"
fmrisc.ProofNavigator.Commands.Induction
Modifier and Type Constant Field Value

public static final java.lang.String Name "induction"
fmrisc.ProofNavigator.Commands.Instantiate
Modifier and Type Constant Field Value

public static final java.lang.String Name "instantiate"
fmrisc.ProofNavigator.Commands.Lemma
Modifier and Type Constant Field Value

public static final java.lang.String Name "lemma"
fmrisc.ProofNavigator.Commands.Next
Modifier and Type Constant Field Value

public static final java.lang.String Name "next"
fmrisc.ProofNavigator.Commands.Open
Modifier and Type Constant Field Value

public static final java.lang.String Name "open"
fmrisc.ProofNavigator.Commands.Option
Modifier and Type Constant Field Value

public static final java.lang.String Name "option"
fmrisc.ProofNavigator.Commands.Prev
Modifier and Type Constant Field Value

public static final java.lang.String Name "prev"
fmrisc.ProofNavigator.Commands.ProofC
Modifier and Type Constant Field Value

public static final java.lang.String Name "proof"
fmrisc.ProofNavigator.Commands.Prove
Modifier and Type Constant Field Value

public static final java.lang.String Name "prove"
fmrisc.ProofNavigator.Commands.Proved
Modifier and Type Constant Field Value

public static final java.lang.String Name "proved"
fmrisc.ProofNavigator.Commands.Quit
Modifier and Type Constant Field Value

public static final java.lang.String Name "quit"
fmrisc.ProofNavigator.Commands.Read
Modifier and Type Constant Field Value

public static final java.lang.String Name "read"
fmrisc.ProofNavigator.Commands.Redo
Modifier and Type Constant Field Value

public static final java.lang.String Name "redo"
fmrisc.ProofNavigator.Commands.Scatter
Modifier and Type Constant Field Value

public static final java.lang.String Name "scatter"
fmrisc.ProofNavigator.Commands.Simplify
Modifier and Type Constant Field Value

public static final java.lang.String Name "simplify"
fmrisc.ProofNavigator.Commands.Skolemize
Modifier and Type Constant Field Value

public static final java.lang.String Name "skolemize"
fmrisc.ProofNavigator.Commands.Split
Modifier and Type Constant Field Value

public static final java.lang.String Name "split"
fmrisc.ProofNavigator.Commands.StateC
Modifier and Type Constant Field Value

public static final java.lang.String Name "state"
fmrisc.ProofNavigator.Commands.TCC
Modifier and Type Constant Field Value

public static final java.lang.String Name "tcc"
fmrisc.ProofNavigator.Commands.TypeAxiom
Modifier and Type Constant Field Value

public static final java.lang.String Name "typeaxiom"
fmrisc.ProofNavigator.Commands.TypeC
Modifier and Type Constant Field Value

public static final java.lang.String Name "printt"
fmrisc.ProofNavigator.Commands.Undo
Modifier and Type Constant Field Value

public static final java.lang.String Name "undo"
fmrisc.ProofNavigator.Commands.ValueC
Modifier and Type Constant Field Value

public static final java.lang.String Name "printv"

fmrisc.ProofNavigator.Communication.PrettyMathML
Modifier and Type Constant Field Value

public static final int WIDTH 85
fmrisc.ProofNavigator.Communication.PrettyPrinter
Modifier and Type Constant Field Value

public static final int WIDTH 75
fmrisc.ProofNavigator.Communication.Store
Modifier and Type Constant Field Value

public static final long HASH_DEFAULT -1L

public static final long STAMP_DEFAULT -1L

fmrisc.ProofNavigator.Proving.CVCL.CVCLParserTokenTypes
Modifier and Type	Constant Field	Value
`public static final int`	`ARROW`	`93`
`public static final int`	`ASSIGNMENT`	`76`
`public static final int`	`BIT`	`95`
`public static final int`	`BITAND`	`88`
`public static final int`	`BITFALSE`	`97`
`public static final int`	`BITNOT`	`90`
`public static final int`	`BITOR`	`85`
`public static final int`	`BITTRUE`	`96`
`public static final int`	`COLON`	`73`
`public static final int`	`COMMA`	`75`
`public static final int`	`COMMENT`	`102`
`public static final int`	`DIGIT`	`99`
`public static final int`	`DIVIDES`	`87`
`public static final int`	`DOTDOT`	`94`
`public static final int`	`EOF`	`1`
`public static final int`	`EOL`	`101`
`public static final int`	`EQUALITY`	`77`
`public static final int`	`EQUIV`	`92`
`public static final int`	`GREATER`	`81`
`public static final int`	`GREATEREQ`	`82`
`public static final int`	`IDENT`	`4`
`public static final int`	`IGNORE`	`63`
`public static final int`	`IMPLIES`	`91`
`public static final int`	`LBRACK`	`66`
`public static final int`	`LBRACKGRID`	`70`
`public static final int`	`LESS`	`79`
`public static final int`	`LESSEQ`	`80`
`public static final int`	`LETTER`	`98`
`public static final int`	`LITERAL_AND`	`33`
`public static final int`	`LITERAL_ARRAY`	`20`
`public static final int`	`LITERAL_BOOLEAN`	`12`
`public static final int`	`LITERAL_ELSE`	`61`
`public static final int`	`LITERAL_ELSIF`	`60`
`public static final int`	`LITERAL_ENDIF`	`62`
`public static final int`	`LITERAL_EXISTS`	`28`
`public static final int`	`LITERAL_FALSE`	`53`
`public static final int`	`LITERAL_FORALL`	`27`
`public static final int`	`LITERAL_IF`	`58`
`public static final int`	`LITERAL_IN`	`25`
`public static final int`	`LITERAL_INT`	`13`
`public static final int`	`LITERAL_LAMBDA`	`26`
`public static final int`	`LITERAL_LET`	`24`
`public static final int`	`LITERAL_NOT`	`34`
`public static final int`	`LITERAL_OF`	`21`
`public static final int`	`LITERAL_OR`	`32`
`public static final int`	`LITERAL_REAL`	`15`
`public static final int`	`LITERAL_SUBTYPE`	`22`
`public static final int`	`LITERAL_THEN`	`59`
`public static final int`	`LITERAL_TRUE`	`52`
`public static final int`	`LITERAL_TYPE`	`6`
`public static final int`	`LITERAL_WITH`	`48`
`public static final int`	`LITERAL_XOR`	`31`
`public static final int`	`LPAR`	`64`
`public static final int`	`LPARGRID`	`68`
`public static final int`	`MINUS`	`84`
`public static final int`	`NONEQUALITY`	`78`
`public static final int`	`NULL_TREE_LOOKAHEAD`	`3`
`public static final int`	`NUMBER`	`50`
`public static final int`	`PERIOD`	`72`
`public static final int`	`PLUS`	`83`
`public static final int`	`POWER`	`89`
`public static final int`	`RBRACK`	`67`
`public static final int`	`RBRACKGRID`	`71`
`public static final int`	`RPAR`	`65`
`public static final int`	`RPARGRID`	`69`
`public static final int`	`SEMICOLON`	`74`
`public static final int`	`TIMES`	`86`
`public static final int`	`WS`	`100`

Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"&&"`
`public static final int`	`precedence`	`4`

Modifier and Type	Constant Field	Value
`public final int`	`max`	`2147483647`
`public final int`	`min`	`-2147483648`

Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"!"`
`public static final int`	`precedence`	`14`

Modifier and Type	Constant Field	Value
`public static final java.lang.String`	`operator`	`"\|\|"`
`public static final int`	`precedence`	`3`

Modifier and Type	Constant Field	Value
`public static final long`	`HASH_DEFAULT`	`-1L`
`public static final long`	`STAMP_DEFAULT`	`-1L`

Constant Field Values

Contents

fmrisc.ProgramExplorer.*

fmrisc.ProofNavigator.*