| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (410 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (164 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (103 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
Global Index
A
AAssignNPC [constructor, in evidence]AAssign_OS [constructor, in operationalSemantics]
AccessArray [definition, in language]
AEval [definition, in language]
AevalCompletes [lemma, in soundnessLemmas]
AevalCompletes [lemma, in evalCompletion]
AExp [constructor, in language]
AExpr [inductive, in language]
Aforall [constructor, in evidence]
AFv [definition, in language]
AFvList [definition, in language]
AId [constructor, in language]
allInDomain [definition, in language]
allVarsIn [definition, in language]
allVarsInASubstA [lemma, in evalCompletion]
allVarsInASubstA [lemma, in soundnessLemmas]
allVarsInASubstA [lemma, in evidenceGenerator]
allVarsInASubstH [lemma, in soundnessLemmas]
allVarsInASubstH [lemma, in evidenceGenerator]
allVarsInASubstH [lemma, in evalCompletion]
allVarsInBSubstA [lemma, in evidenceGenerator]
allVarsInBSubstA [lemma, in soundnessLemmas]
allVarsInBSubstA [lemma, in evalCompletion]
allVarsInBSubstB [lemma, in evalCompletion]
allVarsInBSubstB [lemma, in soundnessLemmas]
allVarsInBSubstB [lemma, in evidenceGenerator]
allVarsInBSubstH [lemma, in evidenceGenerator]
allVarsInBSubstH [lemma, in evalCompletion]
allVarsInBSubstH [lemma, in soundnessLemmas]
allVarsInHSubstA [lemma, in soundnessLemmas]
allVarsInHSubstA [lemma, in evidenceGenerator]
allVarsInHSubstA [lemma, in evalCompletion]
allVarsInHSubstH [lemma, in soundnessLemmas]
allVarsInHSubstH [lemma, in evalCompletion]
allVarsInHSubstH [lemma, in evidenceGenerator]
allVarsInOr [lemma, in varLists]
allVarsInOr [lemma, in evalCompletion]
allVarsInRefl [lemma, in evalCompletion]
allVarsInRefl [lemma, in varLists]
allVarsInSkalVarIn [lemma, in evalCompletion]
allVarsInSkalVarIn [lemma, in varLists]
allVarsInSplit [lemma, in varLists]
allVarsInSplit [lemma, in evalCompletion]
allVarsInTrans [lemma, in varLists]
allVarsInTrans [lemma, in evalCompletion]
aminus [constructor, in language]
amult [constructor, in language]
AndExpr [constructor, in language]
andIntoTheta [definition, in twoAssn]
andIntoThetaFV [lemma, in soundnessLemmas]
andIntoThetaMustExist [lemma, in soundnessLemmas]
andIntoThetaSplit [lemma, in soundnessLemmas]
andIntoThetaTrue [lemma, in soundnessLemmas]
antec [definition, in twoAssn]
antecs [definition, in twoAssn]
antecSet [definition, in twoAssn]
AOp [inductive, in language]
AopExpr [constructor, in language]
AopInter [definition, in language]
AOp_Eq [definition, in language]
AOp_Eq_Eq [lemma, in language]
aplus [constructor, in language]
appCons [lemma, in soundnessLemmas]
app_nil_and [lemma, in soundnessLemmas]
ArrayAccess [constructor, in language]
ASkal [inductive, in language]
ASkalVar [constructor, in language]
Assert [constructor, in language]
AssertNPC [constructor, in evidence]
Assert_OS [constructor, in operationalSemantics]
Assign [constructor, in language]
assnEq_dec [axiom, in twoISoundnessProof]
assnInassns [lemma, in soundnessLemmas]
assns [inductive, in evidence]
Assns [constructor, in evidence]
AState [definition, in language]
ASubstA [definition, in language]
ASubstH [definition, in language]
AsubstRes21A [lemma, in substLemmas]
AsubstRes21H [lemma, in substLemmas]
AsubstValEquivA [lemma, in substLemmas]
AsubstValEquivH [lemma, in substLemmas]
ASynEq [definition, in synEq]
aSynEq_refl [lemma, in synEq]
aSynEq_eq [lemma, in synEq]
aUpdate [definition, in language]
AVal [definition, in language]
AValue [constructor, in language]
B
backSat [definition, in soundness]BAssignNPC [constructor, in evidence]
BAssign_OS [constructor, in operationalSemantics]
BEqCompare [definition, in language]
beql [constructor, in language]
beq_SkalVar_eq [lemma, in synEq]
beq_SkalVar_refl [lemma, in synEq]
beq_SkalVar [definition, in language]
beq_eq_SkalVar [lemma, in synEq]
beq_SkalVar_sem [lemma, in synEq]
BEval [definition, in language]
BevalCompletes [lemma, in soundnessLemmas]
BevalCompletes [lemma, in evalCompletion]
bevalToEval [lemma, in evalCompletion]
bevalToEval [lemma, in soundnessLemmas]
BExp [constructor, in language]
BExpr [inductive, in language]
BFv [definition, in language]
bge [constructor, in language]
bgt [constructor, in language]
BId [constructor, in language]
BinOp2Iand [constructor, in evidence]
BinOp2Iaop [constructor, in evidence]
BinOp2Ibop [constructor, in evidence]
BinOp2Inot [constructor, in evidence]
BinOp2Ior [constructor, in evidence]
ble [constructor, in language]
blt [constructor, in language]
bneql [constructor, in language]
bneq_Skalvar_neq [lemma, in synEq]
BOp [inductive, in language]
BopExpr [constructor, in language]
BOpInter [definition, in language]
BOp_Eq_Eq [lemma, in language]
BOp_Eq [definition, in language]
BSkal [inductive, in language]
BSkalVar [constructor, in language]
BState [definition, in language]
BSubstA [definition, in language]
BSubstB [definition, in language]
BSubstH [definition, in language]
BsubstRes21A [lemma, in substLemmas]
BsubstRes21B [lemma, in substLemmas]
BsubstRes21H [lemma, in substLemmas]
BsubstValEquivA [lemma, in substLemmas]
BsubstValEquivB [lemma, in substLemmas]
BsubstValEquivH [lemma, in substLemmas]
BSynEq [definition, in synEq]
bSynEq_eq [lemma, in synEq]
bSynEq_refl [lemma, in synEq]
bUpdate [definition, in language]
BVal [definition, in language]
BvalExpr [constructor, in language]
BValue [constructor, in language]
BvarExpr [constructor, in language]
C
cmd [definition, in forallTest]Command [inductive, in language]
conBoolAgreement [definition, in twoAssn]
conBoolAgreementFV [lemma, in soundnessLemmas]
conBoolAgreementHelp [definition, in twoAssn]
conBoolAgreementHelpFV [lemma, in soundnessLemmas]
conBoolAgreementMustExist [lemma, in soundnessLemmas]
Cond [constructor, in language]
CondF_OS [constructor, in operationalSemantics]
condMismatch [lemma, in soundnessLemmas]
CondNPC [constructor, in evidence]
CondT_OS [constructor, in operationalSemantics]
ConseqNotModE [constructor, in evidence]
Const2I [constructor, in evidence]
contains [definition, in twoAssn]
containsIn [lemma, in twoAssn]
containsIn [lemma, in twoISoundnessProof]
containsInterp [lemma, in soundnessLemmas]
ContradictionImpl [constructor, in evidence]
Contravar2I [constructor, in evidence]
D
DecisionE [constructor, in evidence]DecisionImpl [constructor, in evidence]
E
eqb_refl [lemma, in synEq]EQEvid [inductive, in evidence]
EQImpl [constructor, in evidence]
EQSound [lemma, in eqSoundness]
EQSoundness [definition, in soundness]
eqSoundness [library]
Eval [definition, in language]
EvalCompletes [lemma, in soundnessLemmas]
EvalCompletes [lemma, in evalCompletion]
evalCompletion [library]
evidence [library]
evidenceGenerator [library]
Expr [inductive, in language]
F
FalseLeftImpl [constructor, in evidence]foldOr [definition, in evidence]
foldOrHelp [definition, in evidence]
foldOrTrueExists [lemma, in soundnessLemmas]
foldOrTrueHelpExists [lemma, in soundnessLemmas]
For [constructor, in language]
ForAllE [constructor, in evidence]
forallTest [library]
ForE_OS [constructor, in operationalSemantics]
For_OS [constructor, in operationalSemantics]
fv [definition, in language]
G
generatePrecondition [definition, in evidenceGenerator]generatePreconditionEvidence [lemma, in evidenceGenerator]
generatePreconditionNotIntroduceVars [lemma, in evidenceGenerator]
generatePreconditionVarsInC [lemma, in evidenceGenerator]
generatePreconditionXcontainsPost [lemma, in evidenceGenerator]
generatePreconditionXIncreases [lemma, in evidenceGenerator]
generatePreconditionXIncreasesS [lemma, in evidenceGenerator]
H
HArray [definition, in language]HAssignNPC [constructor, in evidence]
HAssign_OS [constructor, in operationalSemantics]
HemptyExpr [constructor, in language]
HEval [definition, in language]
HevalCompletes [lemma, in evalCompletion]
HevalCompletes [lemma, in soundnessLemmas]
HExp [constructor, in language]
HExpr [inductive, in language]
HFv [definition, in language]
HId [constructor, in language]
HSkal [inductive, in language]
HSkalVar [constructor, in language]
HState [definition, in language]
HSubstA [definition, in language]
HSubstH [definition, in language]
HsubstRes21A [lemma, in substLemmas]
HsubstRes21H [lemma, in substLemmas]
HsubstValEquivA [lemma, in substLemmas]
HsubstValEquivH [lemma, in substLemmas]
HSynEq [definition, in synEq]
hSynEq_refl [lemma, in synEq]
hSynEq_eq [lemma, in synEq]
hUpdate [definition, in language]
HupdateExpr [constructor, in language]
HVal [definition, in language]
hValToExprSound [lemma, in substLemmas]
hValToHExpr [definition, in language]
HValue [constructor, in language]
HvarExpr [constructor, in language]
I
inAllVarsInTrans [lemma, in varLists]inAllVarsInTrans [lemma, in evalCompletion]
inAntecs [lemma, in soundnessLemmas]
increasingState [lemma, in operationalSemantics]
inDisjunction [definition, in evidence]
InDisjunctionImpl [constructor, in evidence]
inSkalVarInFalse [lemma, in varLists]
InstantiateE [constructor, in evidence]
inSubtract [lemma, in twoISoundnessProof]
IntersectionNull [definition, in varLists]
intersectionNullInNot [lemma, in varLists]
intersectionNullNilTrue [lemma, in varLists]
intersectionNullNotIn [lemma, in varLists]
IntersectionNullP [definition, in varLists]
intersectionNullSubset [lemma, in varLists]
intersectionNullSubset2 [lemma, in varLists]
intersectionNullSubset3 [lemma, in varLists]
intersectionNullSymmetry [lemma, in varLists]
intersectionNullSymmetry2 [lemma, in varLists]
intersectionNullToP [lemma, in varLists]
IntExpr [constructor, in language]
in_trans [lemma, in soundnessLemmas]
isSubstFunctionAB [definition, in evidence]
L
language [library]lookup [definition, in language]
lookupNeqa [lemma, in language]
lookupNeqb [lemma, in language]
lookupNeqh [lemma, in language]
lookupsSameEvalSameA [lemma, in soundnessLemmas]
lookupsSameEvalSameB [lemma, in soundnessLemmas]
lookupsSameEvalSameH [lemma, in soundnessLemmas]
l51 [lemma, in soundnessLemmas]
M
Mods [definition, in language]N
NotExpr [constructor, in language]notModEvalSame [lemma, in soundnessLemmas]
notModEvalSameA [lemma, in soundnessLemmas]
notModEvalSameB [lemma, in soundnessLemmas]
notModEvalSameH [lemma, in soundnessLemmas]
NotModNPC [constructor, in evidence]
NPCEvid [inductive, in evidence]
NPCSound [lemma, in NPCSoundness]
NPCsoundness [definition, in soundness]
NPCSoundness [library]
O
OIEvid [inductive, in evidence]OISound [lemma, in oiSoundness]
OISoundness [definition, in soundness]
oiSoundness [library]
operationalSemantics [library]
Opsem [inductive, in operationalSemantics]
opsemSameEvalSame [lemma, in soundnessLemmas]
opsemSameEvalSameA [lemma, in soundnessLemmas]
opsemSameEvalSameB [lemma, in soundnessLemmas]
opsemSameEvalSameH [lemma, in soundnessLemmas]
OrExpr [constructor, in language]
R
ReflE [constructor, in evidence]RemoveBSubstA [lemma, in substLemmas]
RemoveBSubstH [lemma, in substLemmas]
RhsEquiv2I [constructor, in evidence]
S
Seq [constructor, in language]SeqNPC [constructor, in evidence]
Seq_OS [constructor, in operationalSemantics]
simpleAssign [library]
SkalVar [inductive, in language]
skalVarIn [definition, in language]
skalVarInIn [lemma, in evalCompletion]
skalVarInIn [lemma, in varLists]
skalVarListDifference [definition, in twoAssn]
Skip [constructor, in language]
SkipNPC [constructor, in evidence]
Skip_OS [constructor, in operationalSemantics]
soundness [definition, in soundness]
soundness [library]
soundnessLemmas [library]
soundnessProof [lemma, in soundnessProof]
soundnessProof [library]
splitAllVarsIn [lemma, in evalCompletion]
splitAllVarsIn [lemma, in varLists]
splitBIn [lemma, in soundnessLemmas]
splitIntersectionNull [lemma, in varLists]
State [definition, in language]
subsetTwoAssnsInterpretation [lemma, in soundnessLemmas]
SubstA [definition, in language]
SubstB [definition, in language]
SubstH [definition, in language]
substLemmas [library]
substRes21A [lemma, in substLemmas]
substRes21B [lemma, in substLemmas]
substRes21H [lemma, in substLemmas]
substRes22A [lemma, in substLemmas]
substRes22B [lemma, in substLemmas]
substRes22H [lemma, in substLemmas]
substValEquivA [lemma, in substLemmas]
substValEquivH [lemma, in substLemmas]
subtractAssns [definition, in twoAssn]
subtractAssnsNilSame [lemma, in twoISoundnessProof]
SubtractVars [definition, in varLists]
superSet [definition, in twoAssn]
superSetallIn [lemma, in twoISoundnessProof]
Superset2I [constructor, in evidence]
SvarExpr [constructor, in language]
SymE [constructor, in evidence]
synEq [definition, in synEq]
synEq [library]
SynEqE [constructor, in evidence]
synEq_eq [lemma, in synEq]
T
TAAssignE [constructor, in evidence]TAssertE [constructor, in evidence]
tAssnAppInterp [lemma, in soundnessLemmas]
tAssnInterpApp [lemma, in soundnessLemmas]
tAssnSubtract [lemma, in twoISoundnessProof]
TBAssignE [constructor, in evidence]
TCondE [constructor, in evidence]
TEvid [inductive, in evidence]
THAssignE [constructor, in evidence]
TIEvid [inductive, in evidence]
TNotModE [constructor, in evidence]
TPostImplyE [constructor, in evidence]
TPreImplyE [constructor, in evidence]
TransE [constructor, in evidence]
TransImpl [constructor, in evidence]
Trans2I [constructor, in evidence]
tripleInterp [definition, in soundness]
TrueRightImpl [constructor, in evidence]
TSeqE [constructor, in evidence]
TSkipE [constructor, in evidence]
twoAImp [definition, in soundness]
TwoAssn [definition, in twoAssn]
twoAssn [library]
twoAssnEqual [definition, in twoAssn]
twoAssnEqual_eq [lemma, in twoAssn]
twoAssnEqual_eq2 [lemma, in twoAssn]
twoAssnEq_refl [lemma, in twoAssn]
TwoAssns [definition, in twoAssn]
TwoAssnsFv [definition, in twoAssn]
twoAssnsFvSplit [lemma, in soundnessLemmas]
twoAssnsInterpretation [definition, in soundness]
twoAssnsStatesSymmetry [lemma, in soundnessLemmas]
twoAssnsSubset [lemma, in soundnessLemmas]
TwoAssnsSubst [definition, in twoAssn]
TwoAssnsSubstA [definition, in twoAssn]
twoAssnsSubstAStillAllIn [lemma, in evidenceGenerator]
TwoAssnsSubstB [definition, in twoAssn]
twoAssnsSubstBStillAllIn [lemma, in evidenceGenerator]
TwoAssnsSubstH [definition, in twoAssn]
twoAssnsSubstHStillAllIn [lemma, in evidenceGenerator]
twoAssnsSubstStillAllIn [lemma, in evidenceGenerator]
TwoAssnSubstA [definition, in twoAssn]
TwoAssnSubstB [definition, in twoAssn]
TwoAssnSubstH [definition, in twoAssn]
twoIBack [definition, in soundness]
twoISoundness [definition, in soundness]
twoISoundnessProof [lemma, in twoISoundnessProof]
twoISoundnessProof [library]
TwoSatisfies [constructor, in soundness]
twoSatisfies [inductive, in soundness]
U
UnionE [constructor, in evidence]Union2I [constructor, in evidence]
UpdateArray [definition, in language]
V
vacuous [definition, in twoAssn]vacuousAllFalse [lemma, in twoISoundnessProof]
Vacusous2I [constructor, in evidence]
Val [inductive, in language]
varInEither [lemma, in varLists]
varInEither [lemma, in evalCompletion]
varLists [library]
varsUsedIn [definition, in language]
W
While [constructor, in language]WhileF_OS [constructor, in operationalSemantics]
WhileNPC [constructor, in evidence]
WhileT_OS [constructor, in operationalSemantics]
X
x [definition, in forallTest]Z
ZZeroMax [definition, in operationalSemantics]other
_ ; _ [notation, in language]_ ::= _ [notation, in language]
_ >> _ # [notation, in twoAssn]
_ b|| _ [notation, in language]
_ b&& _ [notation, in language]
ASSERT _ [notation, in language]
FOR _ =1TO _ DO _ [notation, in language]
IFB _ THEN _ ELSE _ FI [notation, in language]
WHILE _ DO _ [notation, in language]
! _ [notation, in language]
[ ] [notation, in language]
[ _ , .. , _ ] [notation, in language]
Lemma Index
A
AevalCompletes [in soundnessLemmas]AevalCompletes [in evalCompletion]
allVarsInASubstA [in evalCompletion]
allVarsInASubstA [in soundnessLemmas]
allVarsInASubstA [in evidenceGenerator]
allVarsInASubstH [in soundnessLemmas]
allVarsInASubstH [in evidenceGenerator]
allVarsInASubstH [in evalCompletion]
allVarsInBSubstA [in evidenceGenerator]
allVarsInBSubstA [in soundnessLemmas]
allVarsInBSubstA [in evalCompletion]
allVarsInBSubstB [in evalCompletion]
allVarsInBSubstB [in soundnessLemmas]
allVarsInBSubstB [in evidenceGenerator]
allVarsInBSubstH [in evidenceGenerator]
allVarsInBSubstH [in evalCompletion]
allVarsInBSubstH [in soundnessLemmas]
allVarsInHSubstA [in soundnessLemmas]
allVarsInHSubstA [in evidenceGenerator]
allVarsInHSubstA [in evalCompletion]
allVarsInHSubstH [in soundnessLemmas]
allVarsInHSubstH [in evalCompletion]
allVarsInHSubstH [in evidenceGenerator]
allVarsInOr [in varLists]
allVarsInOr [in evalCompletion]
allVarsInRefl [in evalCompletion]
allVarsInRefl [in varLists]
allVarsInSkalVarIn [in evalCompletion]
allVarsInSkalVarIn [in varLists]
allVarsInSplit [in varLists]
allVarsInSplit [in evalCompletion]
allVarsInTrans [in varLists]
allVarsInTrans [in evalCompletion]
andIntoThetaFV [in soundnessLemmas]
andIntoThetaMustExist [in soundnessLemmas]
andIntoThetaSplit [in soundnessLemmas]
andIntoThetaTrue [in soundnessLemmas]
AOp_Eq_Eq [in language]
appCons [in soundnessLemmas]
app_nil_and [in soundnessLemmas]
assnInassns [in soundnessLemmas]
AsubstRes21A [in substLemmas]
AsubstRes21H [in substLemmas]
AsubstValEquivA [in substLemmas]
AsubstValEquivH [in substLemmas]
aSynEq_refl [in synEq]
aSynEq_eq [in synEq]
B
beq_SkalVar_eq [in synEq]beq_SkalVar_refl [in synEq]
beq_eq_SkalVar [in synEq]
beq_SkalVar_sem [in synEq]
BevalCompletes [in soundnessLemmas]
BevalCompletes [in evalCompletion]
bevalToEval [in evalCompletion]
bevalToEval [in soundnessLemmas]
bneq_Skalvar_neq [in synEq]
BOp_Eq_Eq [in language]
BsubstRes21A [in substLemmas]
BsubstRes21B [in substLemmas]
BsubstRes21H [in substLemmas]
BsubstValEquivA [in substLemmas]
BsubstValEquivB [in substLemmas]
BsubstValEquivH [in substLemmas]
bSynEq_eq [in synEq]
bSynEq_refl [in synEq]
C
conBoolAgreementFV [in soundnessLemmas]conBoolAgreementHelpFV [in soundnessLemmas]
conBoolAgreementMustExist [in soundnessLemmas]
condMismatch [in soundnessLemmas]
containsIn [in twoAssn]
containsIn [in twoISoundnessProof]
containsInterp [in soundnessLemmas]
E
eqb_refl [in synEq]EQSound [in eqSoundness]
EvalCompletes [in soundnessLemmas]
EvalCompletes [in evalCompletion]
F
foldOrTrueExists [in soundnessLemmas]foldOrTrueHelpExists [in soundnessLemmas]
G
generatePreconditionEvidence [in evidenceGenerator]generatePreconditionNotIntroduceVars [in evidenceGenerator]
generatePreconditionVarsInC [in evidenceGenerator]
generatePreconditionXcontainsPost [in evidenceGenerator]
generatePreconditionXIncreases [in evidenceGenerator]
generatePreconditionXIncreasesS [in evidenceGenerator]
H
HevalCompletes [in evalCompletion]HevalCompletes [in soundnessLemmas]
HsubstRes21A [in substLemmas]
HsubstRes21H [in substLemmas]
HsubstValEquivA [in substLemmas]
HsubstValEquivH [in substLemmas]
hSynEq_refl [in synEq]
hSynEq_eq [in synEq]
hValToExprSound [in substLemmas]
I
inAllVarsInTrans [in varLists]inAllVarsInTrans [in evalCompletion]
inAntecs [in soundnessLemmas]
increasingState [in operationalSemantics]
inSkalVarInFalse [in varLists]
inSubtract [in twoISoundnessProof]
intersectionNullInNot [in varLists]
intersectionNullNilTrue [in varLists]
intersectionNullNotIn [in varLists]
intersectionNullSubset [in varLists]
intersectionNullSubset2 [in varLists]
intersectionNullSubset3 [in varLists]
intersectionNullSymmetry [in varLists]
intersectionNullSymmetry2 [in varLists]
intersectionNullToP [in varLists]
in_trans [in soundnessLemmas]
L
lookupNeqa [in language]lookupNeqb [in language]
lookupNeqh [in language]
lookupsSameEvalSameA [in soundnessLemmas]
lookupsSameEvalSameB [in soundnessLemmas]
lookupsSameEvalSameH [in soundnessLemmas]
l51 [in soundnessLemmas]
N
notModEvalSame [in soundnessLemmas]notModEvalSameA [in soundnessLemmas]
notModEvalSameB [in soundnessLemmas]
notModEvalSameH [in soundnessLemmas]
NPCSound [in NPCSoundness]
O
OISound [in oiSoundness]opsemSameEvalSame [in soundnessLemmas]
opsemSameEvalSameA [in soundnessLemmas]
opsemSameEvalSameB [in soundnessLemmas]
opsemSameEvalSameH [in soundnessLemmas]
R
RemoveBSubstA [in substLemmas]RemoveBSubstH [in substLemmas]
S
skalVarInIn [in evalCompletion]skalVarInIn [in varLists]
soundnessProof [in soundnessProof]
splitAllVarsIn [in evalCompletion]
splitAllVarsIn [in varLists]
splitBIn [in soundnessLemmas]
splitIntersectionNull [in varLists]
subsetTwoAssnsInterpretation [in soundnessLemmas]
substRes21A [in substLemmas]
substRes21B [in substLemmas]
substRes21H [in substLemmas]
substRes22A [in substLemmas]
substRes22B [in substLemmas]
substRes22H [in substLemmas]
substValEquivA [in substLemmas]
substValEquivH [in substLemmas]
subtractAssnsNilSame [in twoISoundnessProof]
superSetallIn [in twoISoundnessProof]
synEq_eq [in synEq]
T
tAssnAppInterp [in soundnessLemmas]tAssnInterpApp [in soundnessLemmas]
tAssnSubtract [in twoISoundnessProof]
twoAssnEqual_eq [in twoAssn]
twoAssnEqual_eq2 [in twoAssn]
twoAssnEq_refl [in twoAssn]
twoAssnsFvSplit [in soundnessLemmas]
twoAssnsStatesSymmetry [in soundnessLemmas]
twoAssnsSubset [in soundnessLemmas]
twoAssnsSubstAStillAllIn [in evidenceGenerator]
twoAssnsSubstBStillAllIn [in evidenceGenerator]
twoAssnsSubstHStillAllIn [in evidenceGenerator]
twoAssnsSubstStillAllIn [in evidenceGenerator]
twoISoundnessProof [in twoISoundnessProof]
V
vacuousAllFalse [in twoISoundnessProof]varInEither [in varLists]
varInEither [in evalCompletion]
Notation Index
other
_ ; _ [in language]_ ::= _ [in language]
_ >> _ # [in twoAssn]
_ b|| _ [in language]
_ b&& _ [in language]
ASSERT _ [in language]
FOR _ =1TO _ DO _ [in language]
IFB _ THEN _ ELSE _ FI [in language]
WHILE _ DO _ [in language]
! _ [in language]
[ ] [in language]
[ _ , .. , _ ] [in language]
Constructor Index
A
AAssignNPC [in evidence]AAssign_OS [in operationalSemantics]
AExp [in language]
Aforall [in evidence]
AId [in language]
aminus [in language]
amult [in language]
AndExpr [in language]
AopExpr [in language]
aplus [in language]
ArrayAccess [in language]
ASkalVar [in language]
Assert [in language]
AssertNPC [in evidence]
Assert_OS [in operationalSemantics]
Assign [in language]
Assns [in evidence]
AValue [in language]
B
BAssignNPC [in evidence]BAssign_OS [in operationalSemantics]
beql [in language]
BExp [in language]
bge [in language]
bgt [in language]
BId [in language]
BinOp2Iand [in evidence]
BinOp2Iaop [in evidence]
BinOp2Ibop [in evidence]
BinOp2Inot [in evidence]
BinOp2Ior [in evidence]
ble [in language]
blt [in language]
bneql [in language]
BopExpr [in language]
BSkalVar [in language]
BvalExpr [in language]
BValue [in language]
BvarExpr [in language]
C
Cond [in language]CondF_OS [in operationalSemantics]
CondNPC [in evidence]
CondT_OS [in operationalSemantics]
ConseqNotModE [in evidence]
Const2I [in evidence]
ContradictionImpl [in evidence]
Contravar2I [in evidence]
D
DecisionE [in evidence]DecisionImpl [in evidence]
E
EQImpl [in evidence]F
FalseLeftImpl [in evidence]For [in language]
ForAllE [in evidence]
ForE_OS [in operationalSemantics]
For_OS [in operationalSemantics]
H
HAssignNPC [in evidence]HAssign_OS [in operationalSemantics]
HemptyExpr [in language]
HExp [in language]
HId [in language]
HSkalVar [in language]
HupdateExpr [in language]
HValue [in language]
HvarExpr [in language]
I
InDisjunctionImpl [in evidence]InstantiateE [in evidence]
IntExpr [in language]
N
NotExpr [in language]NotModNPC [in evidence]
O
OrExpr [in language]R
ReflE [in evidence]RhsEquiv2I [in evidence]
S
Seq [in language]SeqNPC [in evidence]
Seq_OS [in operationalSemantics]
Skip [in language]
SkipNPC [in evidence]
Skip_OS [in operationalSemantics]
Superset2I [in evidence]
SvarExpr [in language]
SymE [in evidence]
SynEqE [in evidence]
T
TAAssignE [in evidence]TAssertE [in evidence]
TBAssignE [in evidence]
TCondE [in evidence]
THAssignE [in evidence]
TNotModE [in evidence]
TPostImplyE [in evidence]
TPreImplyE [in evidence]
TransE [in evidence]
TransImpl [in evidence]
Trans2I [in evidence]
TrueRightImpl [in evidence]
TSeqE [in evidence]
TSkipE [in evidence]
TwoSatisfies [in soundness]
U
UnionE [in evidence]Union2I [in evidence]
V
Vacusous2I [in evidence]W
While [in language]WhileF_OS [in operationalSemantics]
WhileNPC [in evidence]
WhileT_OS [in operationalSemantics]
Inductive Index
A
AExpr [in language]AOp [in language]
ASkal [in language]
assns [in evidence]
B
BExpr [in language]BOp [in language]
BSkal [in language]
C
Command [in language]E
EQEvid [in evidence]Expr [in language]
H
HExpr [in language]HSkal [in language]
N
NPCEvid [in evidence]O
OIEvid [in evidence]Opsem [in operationalSemantics]
S
SkalVar [in language]T
TEvid [in evidence]TIEvid [in evidence]
twoSatisfies [in soundness]
V
Val [in language]Definition Index
A
AccessArray [in language]AEval [in language]
AFv [in language]
AFvList [in language]
allInDomain [in language]
allVarsIn [in language]
andIntoTheta [in twoAssn]
antec [in twoAssn]
antecs [in twoAssn]
antecSet [in twoAssn]
AopInter [in language]
AOp_Eq [in language]
AState [in language]
ASubstA [in language]
ASubstH [in language]
ASynEq [in synEq]
aUpdate [in language]
AVal [in language]
B
backSat [in soundness]BEqCompare [in language]
beq_SkalVar [in language]
BEval [in language]
BFv [in language]
BOpInter [in language]
BOp_Eq [in language]
BState [in language]
BSubstA [in language]
BSubstB [in language]
BSubstH [in language]
BSynEq [in synEq]
bUpdate [in language]
BVal [in language]
C
cmd [in forallTest]conBoolAgreement [in twoAssn]
conBoolAgreementHelp [in twoAssn]
contains [in twoAssn]
E
EQSoundness [in soundness]Eval [in language]
F
foldOr [in evidence]foldOrHelp [in evidence]
fv [in language]
G
generatePrecondition [in evidenceGenerator]H
HArray [in language]HEval [in language]
HFv [in language]
HState [in language]
HSubstA [in language]
HSubstH [in language]
HSynEq [in synEq]
hUpdate [in language]
HVal [in language]
hValToHExpr [in language]
I
inDisjunction [in evidence]IntersectionNull [in varLists]
IntersectionNullP [in varLists]
isSubstFunctionAB [in evidence]
L
lookup [in language]M
Mods [in language]N
NPCsoundness [in soundness]O
OISoundness [in soundness]S
skalVarIn [in language]skalVarListDifference [in twoAssn]
soundness [in soundness]
State [in language]
SubstA [in language]
SubstB [in language]
SubstH [in language]
subtractAssns [in twoAssn]
SubtractVars [in varLists]
superSet [in twoAssn]
synEq [in synEq]
T
tripleInterp [in soundness]twoAImp [in soundness]
TwoAssn [in twoAssn]
twoAssnEqual [in twoAssn]
TwoAssns [in twoAssn]
TwoAssnsFv [in twoAssn]
twoAssnsInterpretation [in soundness]
TwoAssnsSubst [in twoAssn]
TwoAssnsSubstA [in twoAssn]
TwoAssnsSubstB [in twoAssn]
TwoAssnsSubstH [in twoAssn]
TwoAssnSubstA [in twoAssn]
TwoAssnSubstB [in twoAssn]
TwoAssnSubstH [in twoAssn]
twoIBack [in soundness]
twoISoundness [in soundness]
U
UpdateArray [in language]V
vacuous [in twoAssn]varsUsedIn [in language]
X
x [in forallTest]Z
ZZeroMax [in operationalSemantics]Axiom Index
A
assnEq_dec [in twoISoundnessProof]Library Index
E
eqSoundnessevalCompletion
evidence
evidenceGenerator
F
forallTestL
languageN
NPCSoundnessO
oiSoundnessoperationalSemantics
S
simpleAssignsoundness
soundnessLemmas
soundnessProof
substLemmas
synEq
T
twoAssntwoISoundnessProof
V
varLists| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (410 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (164 entries) |
| Notation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (12 entries) |
| Constructor Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (103 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (20 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (92 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (1 entry) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |