| 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 | (1031 entries) |
| Variable 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) |
| 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 | (40 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 | (557 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 | (112 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 | (39 entries) |
| Section 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 | (17 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 | (174 entries) |
Global Index
A
A [variable, in Stalmarck.interImplement2_ex]AaddD [section, in Stalmarck.addArray]
AaddD.a [variable, in Stalmarck.addArray]
AaddD.Ar [variable, in Stalmarck.addArray]
AaddD.b [variable, in Stalmarck.addArray]
AaddD.geta [variable, in Stalmarck.addArray]
AaddD.getb [variable, in Stalmarck.addArray]
AaddD.La [variable, in Stalmarck.addArray]
AaddD.Lb [variable, in Stalmarck.addArray]
AaddD.n [variable, in Stalmarck.addArray]
AaddD.pol [variable, in Stalmarck.addArray]
AaddD.rltab [variable, in Stalmarck.addArray]
AaddD.War [variable, in Stalmarck.addArray]
addArray [library]
addEq [definition, in Stalmarck.state]
addEqComp [lemma, in Stalmarck.state]
addEqInclState [lemma, in Stalmarck.state]
addEqInclState2 [lemma, in Stalmarck.state]
addEqMem [definition, in Stalmarck.memoryImplement]
addEqMemCorrect [lemma, in Stalmarck.memoryImplement]
addEqMem2 [definition, in Stalmarck.memoryImplement]
addEqMem2Correct [lemma, in Stalmarck.memoryImplement]
addEqUnion [lemma, in Stalmarck.unionState]
addInterAux [definition, in Stalmarck.interImplement2]
addInterAuxProp [lemma, in Stalmarck.interImplement2]
algo [section, in Stalmarck.algoDotriplet]
algoDilemma1 [library]
algoDotriplet [library]
algoDotriplets [library]
algoRun [library]
algos [section, in Stalmarck.algoDotriplets]
algoStalmarck [library]
algos.getT [variable, in Stalmarck.algoDotriplets]
algos.getTCorrect [variable, in Stalmarck.algoDotriplets]
algos.LL [variable, in Stalmarck.algoDotriplets]
algoTrace [library]
ANd [constructor, in Stalmarck.normalize]
andSym [lemma, in Stalmarck.restrictState]
append [inductive, in Stalmarck.OrderedListEq]
appendCom [lemma, in Stalmarck.OrderedListEq]
appendDisjIncl1 [lemma, in Stalmarck.OrderedListEq]
appendDisjIncl2 [lemma, in Stalmarck.OrderedListEq]
appendDisjoint [lemma, in Stalmarck.OrderedListEq]
appendEqA [constructor, in Stalmarck.OrderedListEq]
appendEqInv [lemma, in Stalmarck.OrderedListEq]
appendf [definition, in Stalmarck.OrderedListEq]
appendfAppend [lemma, in Stalmarck.OrderedListEq]
appendfDisjoint [lemma, in Stalmarck.OrderedListEq]
appendfInclEq1 [lemma, in Stalmarck.OrderedListEq]
appendfInclEq2 [lemma, in Stalmarck.OrderedListEq]
appendfIncl1 [lemma, in Stalmarck.OrderedListEq]
appendfIncl2 [lemma, in Stalmarck.OrderedListEq]
appendfInv [lemma, in Stalmarck.OrderedListEq]
appendfInvEq [lemma, in Stalmarck.OrderedListEq]
appendfOlist [lemma, in Stalmarck.OrderedListEq]
appendIncl1 [lemma, in Stalmarck.OrderedListEq]
appendIncl2 [lemma, in Stalmarck.OrderedListEq]
appendInv [lemma, in Stalmarck.OrderedListEq]
appendLtA1 [constructor, in Stalmarck.OrderedListEq]
appendLtA2 [constructor, in Stalmarck.OrderedListEq]
appendNil1 [constructor, in Stalmarck.OrderedListEq]
appendNil2 [constructor, in Stalmarck.OrderedListEq]
appendOlist [lemma, in Stalmarck.OrderedListEq]
appendRz [definition, in Stalmarck.addArray]
appendSup [lemma, in Stalmarck.OrderedListEq]
appL [definition, in Stalmarck.algoTrace]
appnat [variable, in Stalmarck.OrderedListEq_ex]
appTrace [definition, in Stalmarck.algoDotriplets]
appTraceCorrect [lemma, in Stalmarck.algoDotriplets]
appZ [variable, in Stalmarck.OrderedListEq_ex]
Auxrem [section, in Stalmarck.PolyListAux]
Auxrem.A [variable, in Stalmarck.PolyListAux]
Auxrem.ADec [variable, in Stalmarck.PolyListAux]
B
B [variable, in Stalmarck.interImplement2_ex]BoolAux [library]
boolDec [definition, in Stalmarck.stalmarck]
boolOp [inductive, in Stalmarck.normalize]
boolOpFun [definition, in Stalmarck.normalize]
BP [variable, in Stalmarck.interImplement2_ex]
buildL [definition, in Stalmarck.algoTrace]
C
C [variable, in Stalmarck.interImplement2_ex]checkTrace [lemma, in Stalmarck.algoTrace]
checkTracef [definition, in Stalmarck.algoTrace]
class [constructor, in Stalmarck.wfArray]
CNat [definition, in Stalmarck.OrderedListEq_ex]
CompInterR [lemma, in Stalmarck.interState]
complete [library]
contradictory [definition, in Stalmarck.state]
contradictoryAddEq [lemma, in Stalmarck.restrictState]
contradictoryEq [lemma, in Stalmarck.algoDotriplet]
contradictoryNotRealize [lemma, in Stalmarck.state]
Contradict1 [lemma, in Stalmarck.sTactic]
Contradict2 [lemma, in Stalmarck.sTactic]
Contradict3 [lemma, in Stalmarck.sTactic]
ContrIncl [lemma, in Stalmarck.state]
ContrInterL [lemma, in Stalmarck.interState]
ContrInterR [lemma, in Stalmarck.interState]
CP [variable, in Stalmarck.interImplement2_ex]
CZ [definition, in Stalmarck.OrderedListEq_ex]
c2 [lemma, in Stalmarck.StalTac_ex]
D
D [variable, in Stalmarck.interImplement2_ex]Deval [section, in Stalmarck.memoryImplement]
Deval.Ar [variable, in Stalmarck.memoryImplement]
Deval.War [variable, in Stalmarck.memoryImplement]
de_morgan4 [lemma, in Stalmarck.BoolAux]
de_morgan3 [lemma, in Stalmarck.BoolAux]
de_morgan2 [lemma, in Stalmarck.BoolAux]
de_morgan1 [lemma, in Stalmarck.BoolAux]
diffElem [definition, in Stalmarck.OrderedListEq]
diffElemNone [lemma, in Stalmarck.OrderedListEq]
diffElemSomeIn [lemma, in Stalmarck.OrderedListEq]
diffElemSomeNIn [lemma, in Stalmarck.OrderedListEq]
DilemmaContrad [lemma, in Stalmarck.complete]
DilemmaContradAux [lemma, in Stalmarck.complete]
dilemmaN [definition, in Stalmarck.algoDilemma1]
dilemmaNCorrect [lemma, in Stalmarck.algoDilemma1]
dilemmaTrace [constructor, in Stalmarck.trace]
dilemmaTraceEval [constructor, in Stalmarck.trace]
dilemma1 [definition, in Stalmarck.algoDilemma1]
dilemma1Correct [lemma, in Stalmarck.algoDilemma1]
dilemma1R [definition, in Stalmarck.algoDilemma1]
dilemma1RCorrect [lemma, in Stalmarck.algoDilemma1]
dilemma1RR [definition, in Stalmarck.algoDilemma1]
dilemma1RRCorrect [lemma, in Stalmarck.algoDilemma1]
dilemma1RRL [definition, in Stalmarck.algoDilemma1]
dilemma1RRLCorrect [lemma, in Stalmarck.algoDilemma1]
DisjbLb [lemma, in Stalmarck.addArray]
DisjLaLc [lemma, in Stalmarck.addArray]
Disjoint [inductive, in Stalmarck.OrderedListEq]
DisjointCom [lemma, in Stalmarck.OrderedListEq]
DisjointCons1 [lemma, in Stalmarck.OrderedListEq]
DisjointCons2 [lemma, in Stalmarck.OrderedListEq]
DisjointDef [constructor, in Stalmarck.OrderedListEq]
Disjointf [lemma, in Stalmarck.OrderedListEq]
DisjointIncl [lemma, in Stalmarck.OrderedListEq]
DisjointInclL [lemma, in Stalmarck.OrderedListEq]
DisjointInclR [lemma, in Stalmarck.OrderedListEq]
DisjointInv1 [lemma, in Stalmarck.OrderedListEq]
DisjointInv2 [lemma, in Stalmarck.OrderedListEq]
DisjointRz [definition, in Stalmarck.memoryImplement]
DisjointRz [definition, in Stalmarck.wfArray]
doTriplet [library]
doTripletAndPpmq [constructor, in Stalmarck.doTriplet]
doTripletAndPpmr [constructor, in Stalmarck.doTriplet]
doTripletAndPpT [constructor, in Stalmarck.doTriplet]
doTripletAndPqF [constructor, in Stalmarck.doTriplet]
doTripletAndPqmr [constructor, in Stalmarck.doTriplet]
doTripletAndPqr [constructor, in Stalmarck.doTriplet]
doTripletAndPqT [constructor, in Stalmarck.doTriplet]
doTripletAndPrF [constructor, in Stalmarck.doTriplet]
doTripletAndPrT [constructor, in Stalmarck.doTriplet]
doTripletBisIncl [lemma, in Stalmarck.doTriplet]
doTripletConfl [lemma, in Stalmarck.doTriplet]
doTripletConflEx [lemma, in Stalmarck.doTriplet]
doTripletCongruent [lemma, in Stalmarck.doTriplets]
doTripletCongruentEx [lemma, in Stalmarck.doTriplet]
doTripletEq [lemma, in Stalmarck.doTriplet]
doTripletEqAux1 [lemma, in Stalmarck.doTriplet]
doTripletEqAux2 [lemma, in Stalmarck.doTriplet]
doTripletEqComp [lemma, in Stalmarck.doTriplet]
doTripletEqCompEx [lemma, in Stalmarck.doTriplet]
doTripletEqMonotone [lemma, in Stalmarck.doTriplet]
doTripletEqPpF [constructor, in Stalmarck.doTriplet]
doTripletEqPpmq [constructor, in Stalmarck.doTriplet]
doTripletEqPpmr [constructor, in Stalmarck.doTriplet]
doTripletEqPpq [constructor, in Stalmarck.doTriplet]
doTripletEqPpr [constructor, in Stalmarck.doTriplet]
doTripletEqPpT [constructor, in Stalmarck.doTriplet]
doTripletEqPqF [constructor, in Stalmarck.doTriplet]
doTripletEqPqmr [constructor, in Stalmarck.doTriplet]
doTripletEqPqr [constructor, in Stalmarck.doTriplet]
doTripletEqPqT [constructor, in Stalmarck.doTriplet]
doTripletEqPrF [constructor, in Stalmarck.doTriplet]
doTripletEqPrT [constructor, in Stalmarck.doTriplet]
doTripletF [definition, in Stalmarck.algoDotriplet]
doTripletFCorrect [lemma, in Stalmarck.algoDotriplet]
doTripletFs [definition, in Stalmarck.algoDotriplets]
doTripletFsCorrect [lemma, in Stalmarck.algoDotriplets]
doTripletFsNCorrect [lemma, in Stalmarck.algoDotriplets]
doTripletFsRCorrect [lemma, in Stalmarck.algoDotriplets]
doTripletIncl [lemma, in Stalmarck.doTriplet]
doTripletInvol [lemma, in Stalmarck.doTriplet]
doTripletInvolEx [lemma, in Stalmarck.doTriplet]
doTripletInvolExAux1 [lemma, in Stalmarck.doTriplet]
doTripletInvolExAux2 [lemma, in Stalmarck.doTriplet]
doTripletMonotoneEx [lemma, in Stalmarck.doTriplet]
doTripletP [inductive, in Stalmarck.doTriplet]
doTripletRestrict [lemma, in Stalmarck.restrictState]
doTripletRestrictAux1 [lemma, in Stalmarck.restrictState]
doTripletRestrictAux2 [lemma, in Stalmarck.restrictState]
doTripletRestrictInv [lemma, in Stalmarck.restrictState]
doTriplets [library]
doTripletsComp [lemma, in Stalmarck.doTriplets]
doTripletsConftEx [lemma, in Stalmarck.doTriplets]
doTripletsExTrace [lemma, in Stalmarck.trace]
doTripletsIncl [lemma, in Stalmarck.doTriplets]
doTripletsInclList [lemma, in Stalmarck.doTriplets]
doTripletsMonotoneEx [lemma, in Stalmarck.doTriplets]
doTripletsN [definition, in Stalmarck.algoDotriplets]
doTripletsP [inductive, in Stalmarck.doTriplets]
doTripletsR [definition, in Stalmarck.algoDotriplets]
doTripletsRealizeStateEval [lemma, in Stalmarck.doTriplets]
doTripletsRef [constructor, in Stalmarck.doTriplets]
doTripletsRestrict [lemma, in Stalmarck.restrictState]
doTripletsRestrictBis [lemma, in Stalmarck.restrictState]
doTripletsRestrictInv [lemma, in Stalmarck.restrictState]
doTripletsRTrans [lemma, in Stalmarck.doTriplets]
doTripletsTermEx [lemma, in Stalmarck.doTriplets]
doTripletsTermExAux [lemma, in Stalmarck.doTriplets]
doTripletsTrans [constructor, in Stalmarck.doTriplets]
doTripletsUnionEx [lemma, in Stalmarck.doTriplets]
doTripletUnionAux1 [lemma, in Stalmarck.doTriplet]
doTripletUnionAux2 [lemma, in Stalmarck.doTriplet]
doTripletUnionEx [lemma, in Stalmarck.doTriplet]
doTripletUnionEx1 [lemma, in Stalmarck.doTriplet]
doTripletUnionEx2 [lemma, in Stalmarck.doTriplet]
DP [variable, in Stalmarck.interImplement2_ex]
Dprop [section, in Stalmarck.memoryImplement]
Dprop.a [variable, in Stalmarck.memoryImplement]
Dprop.Ar [variable, in Stalmarck.memoryImplement]
Dprop.b [variable, in Stalmarck.memoryImplement]
Dprop.geta [variable, in Stalmarck.memoryImplement]
Dprop.getb [variable, in Stalmarck.memoryImplement]
Dprop.La [variable, in Stalmarck.memoryImplement]
Dprop.Lb [variable, in Stalmarck.memoryImplement]
Dprop.pol [variable, in Stalmarck.memoryImplement]
Dprop.rltab [variable, in Stalmarck.memoryImplement]
Dprop.S [variable, in Stalmarck.memoryImplement]
Dprop.SisAr [variable, in Stalmarck.memoryImplement]
Dprop.War [variable, in Stalmarck.memoryImplement]
dT [definition, in Stalmarck.algoDilemma1]
dTCorrect [lemma, in Stalmarck.algoDilemma1]
dubois20 [lemma, in Stalmarck.StalTac_ex]
d2 [variable, in Stalmarck.interImplement2_ex]
d3 [variable, in Stalmarck.interImplement2_ex]
d4 [variable, in Stalmarck.interImplement2_ex]
E
E [variable, in Stalmarck.interImplement2_ex]emptyTrace [constructor, in Stalmarck.trace]
emptyTraceEval [constructor, in Stalmarck.trace]
EP [variable, in Stalmarck.interImplement2_ex]
Eq [constructor, in Stalmarck.normalize]
eqADec [definition, in Stalmarck.OrderedListEq]
EqboolDec [lemma, in Stalmarck.stateExtra]
eqb_com [lemma, in Stalmarck.BoolAux]
eqb_false_b [lemma, in Stalmarck.BoolAux]
eqb_b_false [lemma, in Stalmarck.BoolAux]
eqb_b_true [lemma, in Stalmarck.BoolAux]
eqb_true_b [lemma, in Stalmarck.BoolAux]
eqConstrState [inductive, in Stalmarck.stateDec]
eqConstrStateComp1 [constructor, in Stalmarck.stateDec]
eqConstrStateComp2 [constructor, in Stalmarck.stateDec]
eqConstrStateComp3 [constructor, in Stalmarck.stateDec]
eqConstrStateComp4 [constructor, in Stalmarck.stateDec]
eqConstrStateCons [lemma, in Stalmarck.stateDec]
eqConstrStateContr [constructor, in Stalmarck.stateDec]
eqConstrStateContrGen [lemma, in Stalmarck.stateDec]
eqConstrStateDec [definition, in Stalmarck.stateDec]
eqConstrStateImpeqStateRz [lemma, in Stalmarck.stateDec]
eqConstrStateIn [lemma, in Stalmarck.stateDec]
eqConstrStateInDouble [lemma, in Stalmarck.interState]
eqConstrStateInL [lemma, in Stalmarck.interState]
eqConstrStateInR [lemma, in Stalmarck.interState]
eqConstrStateInv [lemma, in Stalmarck.stateDec]
eqConstrStateNil [constructor, in Stalmarck.stateDec]
eqConstrStateRef [lemma, in Stalmarck.stateDec]
eqConstrStateSimpl [lemma, in Stalmarck.stateDec]
eqConstrStateSym [lemma, in Stalmarck.stateDec]
eqConstrStateTail [constructor, in Stalmarck.stateDec]
eqConstrStateTrans [lemma, in Stalmarck.stateDec]
eqConstrStateTransConstr [lemma, in Stalmarck.stateDec]
EqL [inductive, in Stalmarck.OrderedListEq]
EqLCons [constructor, in Stalmarck.OrderedListEq]
EqLInv [lemma, in Stalmarck.OrderedListEq]
EqLNil [constructor, in Stalmarck.OrderedListEq]
EqLOlist [lemma, in Stalmarck.OrderedListEq]
EqLRef [lemma, in Stalmarck.OrderedListEq]
EqLTrans [lemma, in Stalmarck.OrderedListEq]
eqNotltRz [lemma, in Stalmarck.interImplement]
eqOp [definition, in Stalmarck.Extract]
eqOption [inductive, in Stalmarck.Option]
eqOptionNone [constructor, in Stalmarck.Option]
eqOptionSome [constructor, in Stalmarck.Option]
eqRz [definition, in Stalmarck.rZ]
EqrZComp [lemma, in Stalmarck.memoryImplement]
eqRzComp [lemma, in Stalmarck.rZ]
eqRzElim [lemma, in Stalmarck.triplet]
eqrZRefl [lemma, in Stalmarck.rZ]
eqrZSym [lemma, in Stalmarck.rZ]
eqrZTrans [lemma, in Stalmarck.rZ]
eqState [definition, in Stalmarck.state]
eqStateAddEq [lemma, in Stalmarck.state]
eqStateaddEq1 [lemma, in Stalmarck.state]
eqStateaddEq2 [lemma, in Stalmarck.state]
eqStateContr [lemma, in Stalmarck.state]
eqStateContrSimpl1 [lemma, in Stalmarck.state]
eqStateDec [definition, in Stalmarck.stateDec]
eqStateEq [lemma, in Stalmarck.state]
eqStateEqEvalZ [lemma, in Stalmarck.algoDotriplet]
eqStateEq1 [lemma, in Stalmarck.algoDotriplet]
eqStateEq2 [lemma, in Stalmarck.algoDotriplet]
eqStateEq2EvalZ [lemma, in Stalmarck.algoDotriplet]
eqStateEvalZ [lemma, in Stalmarck.algoDotriplet]
eqStateIncl [lemma, in Stalmarck.state]
eqStateInv [lemma, in Stalmarck.state]
eqStateInvInv [lemma, in Stalmarck.state]
eqStateRarray [lemma, in Stalmarck.algoDotriplets]
eqStateRef [lemma, in Stalmarck.state]
eqStateRz [inductive, in Stalmarck.state]
eqStateRzContr [constructor, in Stalmarck.state]
eqStateRzContrDec [definition, in Stalmarck.stateDec]
eqStateRzContrDec2 [definition, in Stalmarck.complete]
eqStateRzDec [definition, in Stalmarck.stateDec]
eqStateRzIn [constructor, in Stalmarck.state]
eqStateRzInv [constructor, in Stalmarck.state]
eqStateRzPImpeqConstrState [lemma, in Stalmarck.stateDec]
eqStateRzRef [constructor, in Stalmarck.state]
eqStateRzSym [constructor, in Stalmarck.state]
eqStateRzTail [lemma, in Stalmarck.stateDec]
eqStateRzTrans [constructor, in Stalmarck.state]
eqStateSym [lemma, in Stalmarck.state]
eqStateTrans [lemma, in Stalmarck.state]
eqTriv [definition, in Stalmarck.OrderedListEq_ex]
eqTrivZ [definition, in Stalmarck.OrderedListEq_ex]
equalBefore [definition, in Stalmarck.equalBefore]
equalBefore [library]
equalBeforeElim [lemma, in Stalmarck.equalBefore]
equalBeforeExtend [lemma, in Stalmarck.equalBefore]
equalBeforeLt [lemma, in Stalmarck.equalBefore]
equalBeforeMakeTriplets [lemma, in Stalmarck.makeTriplet]
equalBeforeMakeTripletsFun [lemma, in Stalmarck.makeTriplet]
equalBeforeNext [lemma, in Stalmarck.equalBefore]
equalBeforeREval [lemma, in Stalmarck.equalBefore]
equalBeforerZEval [lemma, in Stalmarck.equalBefore]
equalBeforeSym [lemma, in Stalmarck.equalBefore]
equalBeforeTEval [lemma, in Stalmarck.equalBefore]
equalBeforeTrans [lemma, in Stalmarck.equalBefore]
Eval [definition, in Stalmarck.normalize]
evalN [definition, in Stalmarck.memoryImplement]
evalNEvalZ [lemma, in Stalmarck.memoryImplement]
evalRealizeState [lemma, in Stalmarck.doTriplet]
evalRealizeStateAux1 [lemma, in Stalmarck.doTriplet]
evalRealizeStateAux2 [lemma, in Stalmarck.doTriplet]
evalTrace [inductive, in Stalmarck.trace]
evalTraceComp [lemma, in Stalmarck.trace]
evalTraceEq [lemma, in Stalmarck.algoDotriplets]
evalTraceEq [lemma, in Stalmarck.trace]
evalTraceF [definition, in Stalmarck.algoTrace]
evalZ [definition, in Stalmarck.memoryImplement]
evalZComp [lemma, in Stalmarck.memoryImplement]
evalZFalse [lemma, in Stalmarck.memoryImplement]
evalZInv [lemma, in Stalmarck.memoryImplement]
evalZltOr [lemma, in Stalmarck.memoryImplement]
evalZMin [lemma, in Stalmarck.interImplement]
evalZMin [lemma, in Stalmarck.memoryImplement]
evalZTrue [lemma, in Stalmarck.memoryImplement]
Expr [inductive, in Stalmarck.normalize]
ExprToProp [definition, in Stalmarck.refl]
ExprToPropF [lemma, in Stalmarck.refl]
ExprToPropF2 [lemma, in Stalmarck.refl]
ExprToPropTautology [lemma, in Stalmarck.refl]
extendEvalMakeTriplets [lemma, in Stalmarck.makeTriplet]
extendEvalMakeTripletsFun [lemma, in Stalmarck.makeTriplet]
extendFun [definition, in Stalmarck.equalBefore]
extendFunrZEval [lemma, in Stalmarck.equalBefore]
extendFunrZEvalExact [lemma, in Stalmarck.equalBefore]
Extract [library]
F
fappendf [definition, in Stalmarck.OrderedListEq]fappendfAppend [lemma, in Stalmarck.OrderedListEq]
fappendfDisjoint [lemma, in Stalmarck.OrderedListEq]
fappendfInclEq1 [lemma, in Stalmarck.OrderedListEq]
fappendfInclEq2 [lemma, in Stalmarck.OrderedListEq]
fappendfIncl1 [lemma, in Stalmarck.OrderedListEq]
fappendfIncl2 [lemma, in Stalmarck.OrderedListEq]
fappendfInv [lemma, in Stalmarck.OrderedListEq]
fappendfInvEq [lemma, in Stalmarck.OrderedListEq]
fappendfOlist [lemma, in Stalmarck.OrderedListEq]
fappendRz [definition, in Stalmarck.addArray]
fInT [definition, in Stalmarck.algoTrace]
fInTCorrect [lemma, in Stalmarck.algoTrace]
fnAux [definition, in Stalmarck.stateExtra]
forallgetEquivgetRzMin [lemma, in Stalmarck.interImplement]
FStalCorrect [definition, in Stalmarck.algoDotriplets]
FStalCorrectComp [lemma, in Stalmarck.algoDotriplets]
FStalCorrectIncl [lemma, in Stalmarck.algoDotriplets]
FStalCorrect0 [lemma, in Stalmarck.algoDotriplets]
F1 [lemma, in Stalmarck.algoRun]
F2 [lemma, in Stalmarck.algoRun]
F3 [lemma, in Stalmarck.algoRun]
G
geMinIn [lemma, in Stalmarck.OrderedListEq]getB [definition, in Stalmarck.algoRun]
getClassN [definition, in Stalmarck.memoryImplement]
GetClassNProp [lemma, in Stalmarck.memoryImplement]
getClassOlist [lemma, in Stalmarck.memoryImplement]
getEquiv [definition, in Stalmarck.interImplement]
getEquivIdL [lemma, in Stalmarck.interImplement]
getEquivIdR [lemma, in Stalmarck.interImplement]
getEquivInter [lemma, in Stalmarck.interImplement]
getEquivList [definition, in Stalmarck.interImplement]
getEquivListProp1 [lemma, in Stalmarck.interImplement]
getEquivListProp2 [lemma, in Stalmarck.interImplement]
getEquivListProp3 [lemma, in Stalmarck.interImplement]
getEquivListProp4 [lemma, in Stalmarck.interImplement]
getEquivMin [definition, in Stalmarck.interImplement]
getEquivMinEq1 [lemma, in Stalmarck.interImplement]
getEquivMinEq2 [lemma, in Stalmarck.interImplement]
getEquivMinIn1 [lemma, in Stalmarck.interImplement]
getEquivMinIn2 [lemma, in Stalmarck.interImplement]
getEquivMinMin [lemma, in Stalmarck.interImplement]
getEquivMinMinEq [lemma, in Stalmarck.interImplement]
getEquivMinSym [lemma, in Stalmarck.interImplement]
getEquivProp [definition, in Stalmarck.interImplement]
getEquivProp1 [lemma, in Stalmarck.interImplement]
getEquivProp2 [lemma, in Stalmarck.interImplement]
getEquivProp3 [lemma, in Stalmarck.interImplement]
getMin [definition, in Stalmarck.OrderedListEq]
getMinComp [lemma, in Stalmarck.OrderedListEq]
getMinId [definition, in Stalmarck.interImplement]
getMinIdSym [lemma, in Stalmarck.interImplement]
getMinInv [definition, in Stalmarck.interImplement]
getMinInvInd [lemma, in Stalmarck.interImplement]
getMinInvSym [lemma, in Stalmarck.interImplement]
getMinMin [lemma, in Stalmarck.OrderedListEq]
getminnat [variable, in Stalmarck.OrderedListEq_ex]
getMinNone [lemma, in Stalmarck.OrderedListEq]
getminZ [variable, in Stalmarck.OrderedListEq_ex]
getNotIdP [lemma, in Stalmarck.wfArray]
getRzMin [definition, in Stalmarck.interImplement]
getRzMinEq1 [lemma, in Stalmarck.interImplement]
getRzMinEq2 [lemma, in Stalmarck.interImplement]
getRzMinIn1 [lemma, in Stalmarck.interImplement]
getRzMinIn2 [lemma, in Stalmarck.interImplement]
getRzMinMin [lemma, in Stalmarck.interImplement]
getRzMinMinEq [lemma, in Stalmarck.interImplement]
getRzMinSym [lemma, in Stalmarck.interImplement]
getRzMinUnique [lemma, in Stalmarck.interImplement]
getT [definition, in Stalmarck.algoTrace]
getTCorrect [lemma, in Stalmarck.algoTrace]
I
Impl [constructor, in Stalmarck.normalize]implb_elim [lemma, in Stalmarck.BoolAux]
implb_false_b [lemma, in Stalmarck.BoolAux]
implb_true_b [lemma, in Stalmarck.BoolAux]
implb_b_false [lemma, in Stalmarck.BoolAux]
implb_b_true [lemma, in Stalmarck.BoolAux]
InclEq [inductive, in Stalmarck.OrderedListEq]
InclEqCons [lemma, in Stalmarck.OrderedListEq]
InclEqDef [constructor, in Stalmarck.OrderedListEq]
InclEqNil [lemma, in Stalmarck.OrderedListEq]
InclEqOlist [lemma, in Stalmarck.OrderedListEq]
InclEqRef [lemma, in Stalmarck.OrderedListEq]
InclEqTrans [lemma, in Stalmarck.OrderedListEq]
inclImpImplEq [lemma, in Stalmarck.OrderedListEq]
inclState [definition, in Stalmarck.state]
inclStateAddEq [lemma, in Stalmarck.state]
inclStateAddEqInv [lemma, in Stalmarck.state]
inclStateDec [definition, in Stalmarck.stateDec]
inclStateDecBis [definition, in Stalmarck.stateDec]
inclStateEqStateComp [lemma, in Stalmarck.state]
inclStateIn [lemma, in Stalmarck.state]
inclStateRef [lemma, in Stalmarck.state]
inclStateTrans [lemma, in Stalmarck.state]
InDec [definition, in Stalmarck.algoTrace]
InEq [inductive, in Stalmarck.OrderedListEq]
InEqComp [lemma, in Stalmarck.OrderedListEq]
InEqDec [definition, in Stalmarck.OrderedListEq]
InEqHead [constructor, in Stalmarck.OrderedListEq]
InEqInv [lemma, in Stalmarck.wfArray]
InEqNList [lemma, in Stalmarck.OrderedListEq]
InEqOlistInv [lemma, in Stalmarck.OrderedListEq]
InEqSkip [constructor, in Stalmarck.OrderedListEq]
InEqSup [lemma, in Stalmarck.OrderedListEq]
inExpr [inductive, in Stalmarck.refl]
inExprDec [definition, in Stalmarck.refl]
inImpInEq [lemma, in Stalmarck.OrderedListEq]
initCorrect [lemma, in Stalmarck.memoryImplement]
inLt [lemma, in Stalmarck.equalBefore]
inMapComp [lemma, in Stalmarck.interImplement]
inN [constructor, in Stalmarck.refl]
inNodeLeft [constructor, in Stalmarck.refl]
inNodeRight [constructor, in Stalmarck.refl]
InRestrictState [lemma, in Stalmarck.restrictState]
inRExpr [inductive, in Stalmarck.normalize]
inRN [constructor, in Stalmarck.normalize]
inRNodeLeft [constructor, in Stalmarck.normalize]
inRNodeRight [constructor, in Stalmarck.normalize]
inRV [constructor, in Stalmarck.normalize]
InRz [definition, in Stalmarck.memoryImplement]
InRz [definition, in Stalmarck.wfArray]
InRzDec [lemma, in Stalmarck.wfArray]
InState [lemma, in Stalmarck.restrictState]
inter [section, in Stalmarck.interImplement]
inter [section, in Stalmarck.interImplement2]
inter [inductive, in Stalmarck.OrderedListEq]
interAssoc [lemma, in Stalmarck.interState]
interCom [lemma, in Stalmarck.OrderedListEq]
interEqA [constructor, in Stalmarck.OrderedListEq]
interf [definition, in Stalmarck.OrderedListEq]
interfCom [lemma, in Stalmarck.OrderedListEq]
interfIncl1 [lemma, in Stalmarck.OrderedListEq]
interfIncl2 [lemma, in Stalmarck.OrderedListEq]
interfMin [lemma, in Stalmarck.OrderedListEq]
interfOlist [lemma, in Stalmarck.OrderedListEq]
interfProp1 [lemma, in Stalmarck.OrderedListEq]
interImplement [library]
interImplement2 [library]
interImplement2_ex [library]
interIncl1 [lemma, in Stalmarck.OrderedListEq]
interIncl2 [lemma, in Stalmarck.OrderedListEq]
interLtA1 [constructor, in Stalmarck.OrderedListEq]
interLtA2 [constructor, in Stalmarck.OrderedListEq]
interMem [definition, in Stalmarck.interImplement2]
interMemEqStateRz [lemma, in Stalmarck.interState]
interMemInL [lemma, in Stalmarck.interState]
interMemInR [lemma, in Stalmarck.interState]
interMemMin [lemma, in Stalmarck.interState]
interMemProp [lemma, in Stalmarck.interState]
interMemProp [definition, in Stalmarck.interImplement2]
interMin [lemma, in Stalmarck.OrderedListEq]
internat [variable, in Stalmarck.OrderedListEq_ex]
interNil1 [constructor, in Stalmarck.OrderedListEq]
interNil2 [constructor, in Stalmarck.OrderedListEq]
interOlist [lemma, in Stalmarck.OrderedListEq]
interState [definition, in Stalmarck.interState]
interState [library]
interStateEq [lemma, in Stalmarck.interState]
interStateP [definition, in Stalmarck.interState]
interStatePEq [lemma, in Stalmarck.interState]
interStatePIncl [lemma, in Stalmarck.interState]
interStatePInclSelf [lemma, in Stalmarck.interState]
interStatePRef [lemma, in Stalmarck.interState]
interStatePSym [lemma, in Stalmarck.interState]
interStateSym [lemma, in Stalmarck.interState]
interSup [lemma, in Stalmarck.OrderedListEq]
interZ [variable, in Stalmarck.OrderedListEq_ex]
inTriplet [definition, in Stalmarck.triplet]
inTripletDec [definition, in Stalmarck.triplet]
inTriplets [definition, in Stalmarck.triplet]
inTripletsComp [lemma, in Stalmarck.triplet]
inTripletsCompInv [lemma, in Stalmarck.triplet]
inTripletsDec [definition, in Stalmarck.triplet]
inTripletsFalse [lemma, in Stalmarck.triplet]
inTripletsIn [lemma, in Stalmarck.triplet]
inTripletsTrue [lemma, in Stalmarck.triplet]
inTripletsVarTriplet [lemma, in Stalmarck.triplet]
inV [constructor, in Stalmarck.refl]
L
LB [variable, in Stalmarck.interImplement2_ex]LC [variable, in Stalmarck.interImplement2_ex]
LD [variable, in Stalmarck.interImplement2_ex]
lePlusComp [lemma, in Stalmarck.ltState]
letP [definition, in Stalmarck.memoryImplement]
LetP [definition, in Stalmarck.LetP]
LetP [library]
liftRz [definition, in Stalmarck.rZ]
listDec [definition, in Stalmarck.wfArray]
lt [section, in Stalmarck.ltState]
ltlePlusCompL [lemma, in Stalmarck.ltState]
ltlePlusCompR [lemma, in Stalmarck.ltState]
ltState [definition, in Stalmarck.ltState]
ltState [library]
ltStateEqComp [lemma, in Stalmarck.ltState]
ltStateLt [lemma, in Stalmarck.ltState]
ltStateTrans [lemma, in Stalmarck.ltState]
ltStateWf [lemma, in Stalmarck.ltState]
lt.L [variable, in Stalmarck.ltState]
l1 [variable, in Stalmarck.OrderedListEq_ex]
l2 [variable, in Stalmarck.OrderedListEq_ex]
M
makeTriplet [library]makeTriplets [definition, in Stalmarck.makeTriplet]
makeTripletsFun [definition, in Stalmarck.makeTriplet]
makeTripletsFunIncl [lemma, in Stalmarck.makeTriplet]
makeTripletsFunIncr [lemma, in Stalmarck.makeTriplet]
makeTripletsFunMax [lemma, in Stalmarck.makeTriplet]
makeTripletsIn [lemma, in Stalmarck.makeTriplet]
map_id [lemma, in Stalmarck.PolyListAux]
max [definition, in Stalmarck.rZ]
maxProp1 [lemma, in Stalmarck.rZ]
maxProp2 [lemma, in Stalmarck.rZ]
maxProp3 [lemma, in Stalmarck.rZ]
maxProp4 [lemma, in Stalmarck.rZ]
maxProp5 [lemma, in Stalmarck.rZ]
maxProp6 [lemma, in Stalmarck.rZ]
maxVar [definition, in Stalmarck.normalize]
maxVarTriplet [definition, in Stalmarck.triplet]
maxVarTriplets [definition, in Stalmarck.triplet]
maxVarTripletsRlt [lemma, in Stalmarck.makeTriplet]
mbD [definition, in Stalmarck.memoryImplement]
mbDOp [definition, in Stalmarck.memoryImplement]
mbDT [definition, in Stalmarck.algoDotriplets]
mbDTOp [definition, in Stalmarck.algoDotriplets]
memoryImplement [library]
min [definition, in Stalmarck.rZ]
minProp1 [lemma, in Stalmarck.rZ]
minProp2 [lemma, in Stalmarck.rZ]
minProp3 [lemma, in Stalmarck.rZ]
minProp4 [lemma, in Stalmarck.rZ]
minProp5 [lemma, in Stalmarck.rZ]
minProp6 [lemma, in Stalmarck.rZ]
myNth [definition, in Stalmarck.complete]
N
N [constructor, in Stalmarck.normalize]Ncount [definition, in Stalmarck.ltState]
NcountLe [lemma, in Stalmarck.ltState]
NcountLt [lemma, in Stalmarck.ltState]
negbElim [lemma, in Stalmarck.stateExtra]
negRealizeTriplets [lemma, in Stalmarck.complete]
Node [constructor, in Stalmarck.normalize]
None [constructor, in Stalmarck.Option]
norm [definition, in Stalmarck.normalize]
normalize [library]
normEval [lemma, in Stalmarck.normalize]
normImpl [definition, in Stalmarck.normalize]
normImplEval [lemma, in Stalmarck.normalize]
normNot [definition, in Stalmarck.normalize]
normNotEval [lemma, in Stalmarck.normalize]
normOr [definition, in Stalmarck.normalize]
normOrEval [lemma, in Stalmarck.normalize]
NotEqComp [lemma, in Stalmarck.rZ]
NotInAppendf [lemma, in Stalmarck.OrderedListEq]
NotInCons1 [lemma, in Stalmarck.PolyListAux]
NotInEqComp [lemma, in Stalmarck.OrderedListEq]
notrltzero [lemma, in Stalmarck.memoryImplement]
Nrel [definition, in Stalmarck.ltState]
NrelLe [lemma, in Stalmarck.ltState]
NrelLt [lemma, in Stalmarck.ltState]
nthTail [definition, in Stalmarck.complete]
nthTailProp1 [lemma, in Stalmarck.complete]
nthTailProp2 [lemma, in Stalmarck.complete]
nthTailProp3 [lemma, in Stalmarck.complete]
O
odilemma1 [section, in Stalmarck.algoDilemma1]odilemma1.getT [variable, in Stalmarck.algoDilemma1]
odilemma1.getTCorrect [variable, in Stalmarck.algoDilemma1]
odilemma1.LL [variable, in Stalmarck.algoDilemma1]
odilemma1.n [variable, in Stalmarck.algoDilemma1]
Olist [inductive, in Stalmarck.OrderedListEq]
OlistArray [inductive, in Stalmarck.wfArray]
OlistArrayDef [constructor, in Stalmarck.wfArray]
OlistCons [constructor, in Stalmarck.OrderedListEq]
olistDiff [definition, in Stalmarck.OrderedListEq]
Olistf [lemma, in Stalmarck.OrderedListEq]
OlistIn [lemma, in Stalmarck.OrderedListEq]
OlistInv [lemma, in Stalmarck.OrderedListEq]
OlistNil [constructor, in Stalmarck.OrderedListEq]
OlistOne [constructor, in Stalmarck.OrderedListEq]
OlistRz [definition, in Stalmarck.memoryImplement]
OlistRz [definition, in Stalmarck.wfArray]
OlistSkip [lemma, in Stalmarck.OrderedListEq]
OlistSup [lemma, in Stalmarck.OrderedListEq]
OlistSupEq [lemma, in Stalmarck.OrderedListEq]
OlistUnique [lemma, in Stalmarck.OrderedListEq]
OlistUniqueEq [lemma, in Stalmarck.OrderedListEq]
oneState [definition, in Stalmarck.ltState]
oneStateAll [definition, in Stalmarck.ltState]
oneStateAllLe [lemma, in Stalmarck.ltState]
oneStateAllLt [lemma, in Stalmarck.ltState]
oneStateLe [lemma, in Stalmarck.ltState]
oneStateLt [lemma, in Stalmarck.ltState]
Option [inductive, in Stalmarck.Option]
Option [library]
Or [constructor, in Stalmarck.normalize]
orb_false_2 [lemma, in Stalmarck.BoolAux]
orb_false_1 [lemma, in Stalmarck.BoolAux]
OrderedList [section, in Stalmarck.OrderedListEq]
OrderedListEq [library]
OrderedListEq_ex [library]
OrderedList.A [variable, in Stalmarck.OrderedListEq]
OrderedList.eqA [variable, in Stalmarck.OrderedListEq]
OrderedList.eqADec' [variable, in Stalmarck.OrderedListEq]
OrderedList.eqARefl [variable, in Stalmarck.OrderedListEq]
OrderedList.eqASym [variable, in Stalmarck.OrderedListEq]
OrderedList.eqATrans [variable, in Stalmarck.OrderedListEq]
OrderedList.f [variable, in Stalmarck.OrderedListEq]
OrderedList.feqA [variable, in Stalmarck.OrderedListEq]
OrderedList.ltA [variable, in Stalmarck.OrderedListEq]
OrderedList.ltAAnti [variable, in Stalmarck.OrderedListEq]
OrderedList.ltADec [variable, in Stalmarck.OrderedListEq]
OrderedList.ltAeqAComp [variable, in Stalmarck.OrderedListEq]
OrderedList.ltAImpNotEqA [variable, in Stalmarck.OrderedListEq]
OrderedList.ltAntiSym [variable, in Stalmarck.OrderedListEq]
OrderedList.ltATrans [variable, in Stalmarck.OrderedListEq]
OrderedList.test [variable, in Stalmarck.OrderedListEq]
OrderedList.testDec [variable, in Stalmarck.OrderedListEq]
OrderedList.testEq [variable, in Stalmarck.OrderedListEq]
orun [section, in Stalmarck.algoRun]
orun.t1 [variable, in Stalmarck.algoRun]
orun.t2 [variable, in Stalmarck.algoRun]
ostal [section, in Stalmarck.algoStalmarck]
ostal.getT [variable, in Stalmarck.algoStalmarck]
ostal.getTCorrect [variable, in Stalmarck.algoStalmarck]
ostal.LL [variable, in Stalmarck.algoStalmarck]
ostal.n [variable, in Stalmarck.algoStalmarck]
P
PNone [constructor, in Stalmarck.refl]pointerDecrease [inductive, in Stalmarck.wfArray]
pointerDecreaseDef [constructor, in Stalmarck.wfArray]
pointToClassClass [inductive, in Stalmarck.wfArray]
pointToClassClassRef [constructor, in Stalmarck.wfArray]
pointToClassRef [inductive, in Stalmarck.wfArray]
pointToClassRefDef [constructor, in Stalmarck.wfArray]
PolyListAux [library]
POption [inductive, in Stalmarck.refl]
Praeclarum [lemma, in Stalmarck.StalTac_ex]
prodRz [definition, in Stalmarck.interState]
prodRzInL [lemma, in Stalmarck.restrictState]
prodRzInR [lemma, in Stalmarck.restrictState]
prodRzProp [lemma, in Stalmarck.interState]
PSome [constructor, in Stalmarck.refl]
puz002_1 [lemma, in Stalmarck.StalTac_ex]
puz003_1 [lemma, in Stalmarck.StalTac_ex]
Q
quatuor [constructor, in Stalmarck.algoDotriplets]Quatuor [inductive, in Stalmarck.algoDotriplets]
R
rA [section, in Stalmarck.rZ]rA [section, in Stalmarck.refl]
rAnd [constructor, in Stalmarck.normalize]
rArray [inductive, in Stalmarck.rZ]
rArrayContradictory [lemma, in Stalmarck.interImplement2]
rArrayDef [lemma, in Stalmarck.rZ]
rArrayDefP [lemma, in Stalmarck.refl]
rArrayDef1 [lemma, in Stalmarck.rZ]
rArrayDef1P [lemma, in Stalmarck.refl]
rArrayDef2 [lemma, in Stalmarck.rZ]
rArrayDef2P [lemma, in Stalmarck.refl]
rArrayGet [definition, in Stalmarck.rZ]
rArrayGetEvalN [lemma, in Stalmarck.memoryImplement]
rArrayGetEvalZ [lemma, in Stalmarck.memoryImplement]
rArrayGetP [definition, in Stalmarck.refl]
rArrayInit [definition, in Stalmarck.rZ]
rArrayInitP [definition, in Stalmarck.refl]
rArrayMake [constructor, in Stalmarck.rZ]
rArrayMakeP [constructor, in Stalmarck.refl]
rArrayP [inductive, in Stalmarck.refl]
rArraySet [definition, in Stalmarck.rZ]
rArraySetList [definition, in Stalmarck.addArray]
rArraySetListInv1 [lemma, in Stalmarck.addArray]
rArraySetListInv2 [lemma, in Stalmarck.addArray]
rArraySetP [definition, in Stalmarck.refl]
rArrayState [definition, in Stalmarck.memoryImplement]
rArrayStateDef1 [lemma, in Stalmarck.memoryImplement]
rArrayStateDef2 [lemma, in Stalmarck.memoryImplement]
rArrayStateEqState [lemma, in Stalmarck.memoryImplement]
rArrayStateGet [lemma, in Stalmarck.memoryImplement]
rA.A [variable, in Stalmarck.rZ]
rBoolOp [inductive, in Stalmarck.normalize]
rBoolOpDec [definition, in Stalmarck.triplet]
rBoolOpFun [definition, in Stalmarck.normalize]
Realizable [lemma, in Stalmarck.stateExtra]
RealizableAux1 [lemma, in Stalmarck.stateExtra]
RealizableAux2 [lemma, in Stalmarck.stateExtra]
RealizableAux3 [lemma, in Stalmarck.stateExtra]
RealizableCstr [lemma, in Stalmarck.stateExtra]
Realizable2 [lemma, in Stalmarck.stateExtra]
RealizeNegb [lemma, in Stalmarck.stateExtra]
realizeState [definition, in Stalmarck.state]
realizeStateAddEq [lemma, in Stalmarck.state]
realizeStateEval [lemma, in Stalmarck.doTriplet]
realizeStateEvalAux1 [lemma, in Stalmarck.doTriplet]
realizeStateEvalAux2 [lemma, in Stalmarck.doTriplet]
realizeStateEvalEquiv [lemma, in Stalmarck.doTriplet]
realizeStateIncl [lemma, in Stalmarck.state]
realizeStateInclInv [lemma, in Stalmarck.stateExtra]
realizeStateInv [lemma, in Stalmarck.state]
realizeStateInvAddEq [lemma, in Stalmarck.state]
realizeStateInvAddEq2 [lemma, in Stalmarck.state]
realizeStateInvComp [lemma, in Stalmarck.state]
realizeStateNil [lemma, in Stalmarck.state]
realizeTripletCons [lemma, in Stalmarck.triplet]
realizeTripletIncl [lemma, in Stalmarck.triplet]
realizeTripletNil [lemma, in Stalmarck.triplet]
realizeTriplets [definition, in Stalmarck.triplet]
RealizeTripletsDec [definition, in Stalmarck.complete]
ref [constructor, in Stalmarck.wfArray]
refl [section, in Stalmarck.refl]
refl [library]
refl.fmap [variable, in Stalmarck.refl]
refl.fmapO [variable, in Stalmarck.refl]
refSameEq [lemma, in Stalmarck.wfArray]
rem [definition, in Stalmarck.PolyListAux]
remEq [lemma, in Stalmarck.PolyListAux]
remIn [lemma, in Stalmarck.PolyListAux]
remNotIn [lemma, in Stalmarck.PolyListAux]
rEmpty [constructor, in Stalmarck.rZ]
rEmptyP [constructor, in Stalmarck.refl]
remSizeLess [lemma, in Stalmarck.PolyListAux]
rEq [constructor, in Stalmarck.normalize]
restricMonotone [lemma, in Stalmarck.restrictState]
RestrictAddEq [lemma, in Stalmarck.restrictState]
RestrictAddEq1 [lemma, in Stalmarck.restrictState]
RestrictAddEq2 [lemma, in Stalmarck.restrictState]
restrictContradiction [lemma, in Stalmarck.restrictState]
restrictDoTripletComp [lemma, in Stalmarck.restrictState]
restrictDoTripletCompAux1 [lemma, in Stalmarck.restrictState]
restrictDoTripletCompAux2 [lemma, in Stalmarck.restrictState]
restrictDoTripletsComp [lemma, in Stalmarck.restrictState]
restrictDoTripletsCompAux1 [lemma, in Stalmarck.restrictState]
restrictEqComp [lemma, in Stalmarck.restrictState]
restrictState [definition, in Stalmarck.restrictState]
restrictState [library]
restrictStateComp [lemma, in Stalmarck.restrictState]
restrictStateIncl [lemma, in Stalmarck.restrictState]
restrictStateInvol [lemma, in Stalmarck.restrictState]
restrictStateInZeroL [lemma, in Stalmarck.restrictState]
restrictStateInZeroR [lemma, in Stalmarck.restrictState]
ResTriplet [definition, in Stalmarck.restrictState]
ResTripletInResTriplets [lemma, in Stalmarck.restrictState]
ResTriplets [definition, in Stalmarck.restrictState]
rEval [definition, in Stalmarck.normalize]
rExpr [inductive, in Stalmarck.normalize]
rIwF [lemma, in Stalmarck.algoTrace]
rlt [definition, in Stalmarck.rZ]
rltAntiSym [lemma, in Stalmarck.rZ]
rltDec [definition, in Stalmarck.rZ]
rltDef2 [lemma, in Stalmarck.rZ]
rltEDec [definition, in Stalmarck.rZ]
rltNotRefl [lemma, in Stalmarck.rZ]
rltRmaxLeft [lemma, in Stalmarck.rZ]
rltRmaxRight [lemma, in Stalmarck.rZ]
rltRnext2Inv [lemma, in Stalmarck.rZ]
rltTrans [lemma, in Stalmarck.rZ]
rltTransRnext1 [lemma, in Stalmarck.rZ]
rltTransRnext2 [lemma, in Stalmarck.rZ]
rmax [definition, in Stalmarck.rZ]
rmaxRlt [lemma, in Stalmarck.rZ]
rmaxRltLeft [lemma, in Stalmarck.rZ]
rmaxRltRight [lemma, in Stalmarck.rZ]
rN [constructor, in Stalmarck.normalize]
rNat [definition, in Stalmarck.rZ]
rNatDec [definition, in Stalmarck.rZ]
rnext [definition, in Stalmarck.rZ]
rNextInv [lemma, in Stalmarck.rZ]
rnextMono [lemma, in Stalmarck.rZ]
rnextNotZero [lemma, in Stalmarck.rZ]
rnextRlt [lemma, in Stalmarck.rZ]
rNextS [lemma, in Stalmarck.rZ]
rNode [constructor, in Stalmarck.normalize]
rSplit [constructor, in Stalmarck.rZ]
rSplitP [constructor, in Stalmarck.refl]
rTautology [definition, in Stalmarck.normalize]
rTautotTauto [lemma, in Stalmarck.makeTriplet]
rTree [inductive, in Stalmarck.rZ]
rTreeDef1 [lemma, in Stalmarck.rZ]
rTreeDef1P [lemma, in Stalmarck.refl]
rTreeDef2 [lemma, in Stalmarck.rZ]
rTreeDef2 [lemma, in Stalmarck.refl]
rTreeGet [definition, in Stalmarck.rZ]
rTreeGetP [definition, in Stalmarck.refl]
rTreeP [inductive, in Stalmarck.refl]
rTreeSet [definition, in Stalmarck.rZ]
rTreeSetP [definition, in Stalmarck.refl]
run [definition, in Stalmarck.algoRun]
runC [lemma, in Stalmarck.algoRun]
runCorrect [lemma, in Stalmarck.algoRun]
rV [constructor, in Stalmarck.normalize]
rVlt [definition, in Stalmarck.rZ]
rVltrZComp [lemma, in Stalmarck.rZ]
rZ [inductive, in Stalmarck.rZ]
rZ [library]
rZComp [definition, in Stalmarck.rZ]
rZCompEq [lemma, in Stalmarck.rZ]
rZCompInv [lemma, in Stalmarck.rZ]
rZCompInvol [lemma, in Stalmarck.rZ]
rZCompInvolList [lemma, in Stalmarck.interImplement]
rZDec [definition, in Stalmarck.rZ]
rZEval [definition, in Stalmarck.triplet]
rZEvalCompInv [lemma, in Stalmarck.state]
rZEvalEvalRZMakeTriplets [lemma, in Stalmarck.makeTriplet]
rZEvalREvalMakeTriplets [lemma, in Stalmarck.makeTriplet]
rZFalse [definition, in Stalmarck.rZ]
rZlt [definition, in Stalmarck.rZ]
rZltAntiSym [lemma, in Stalmarck.rZ]
rZltDec [definition, in Stalmarck.rZ]
rZltDef2 [lemma, in Stalmarck.rZ]
rZltEDec [definition, in Stalmarck.rZ]
rZltEqComp [lemma, in Stalmarck.rZ]
rZltNotRefl [lemma, in Stalmarck.rZ]
rZltTrans [lemma, in Stalmarck.rZ]
rZMinus [constructor, in Stalmarck.rZ]
rZPlus [constructor, in Stalmarck.rZ]
rZSignDec [definition, in Stalmarck.rZ]
rZTrue [definition, in Stalmarck.rZ]
S
samePol [definition, in Stalmarck.rZ]samePolRz [definition, in Stalmarck.rZ]
samePolRzComp [lemma, in Stalmarck.rZ]
samePolRzEqRz [lemma, in Stalmarck.rZ]
samePolRzInvRvlt [lemma, in Stalmarck.rZ]
samePolRzRvlt [lemma, in Stalmarck.rZ]
samePolRzsamePolRz [lemma, in Stalmarck.rZ]
samePolRzValRz [lemma, in Stalmarck.rZ]
samePolSamePolRz [lemma, in Stalmarck.rZ]
seqTrace [constructor, in Stalmarck.trace]
seqTraceEval [constructor, in Stalmarck.trace]
Some [constructor, in Stalmarck.Option]
SomeComp [lemma, in Stalmarck.Option]
sTactic [library]
stal [definition, in Stalmarck.algoStalmarck]
stalCorrect [lemma, in Stalmarck.algoStalmarck]
stalmarck [library]
stalmarckComp [lemma, in Stalmarck.stalmarck]
stalmarckComplete [lemma, in Stalmarck.complete]
stalmarckCorrect [lemma, in Stalmarck.stalmarck]
stalmarckExTrace [lemma, in Stalmarck.trace]
stalmarckGivesValidEquation [lemma, in Stalmarck.stalmarck]
stalmarckIncl [lemma, in Stalmarck.stalmarck]
stalmarckInclList [lemma, in Stalmarck.algoDotriplets]
stalmarckMonotoneEx [lemma, in Stalmarck.stalmarck]
stalmarckP [inductive, in Stalmarck.stalmarck]
stalmarckPref [constructor, in Stalmarck.stalmarck]
stalmarckPSplit [constructor, in Stalmarck.stalmarck]
stalmarckRealizeStateEval [lemma, in Stalmarck.stalmarck]
stalmarckTrans [constructor, in Stalmarck.stalmarck]
stalmarckUnionEx [lemma, in Stalmarck.stalmarck]
stalN [definition, in Stalmarck.algoStalmarck]
stalNCorrect [lemma, in Stalmarck.algoStalmarck]
StalTac [library]
StalTac_ex [library]
State [definition, in Stalmarck.state]
state [library]
stateAssignContrad [lemma, in Stalmarck.complete]
stateAssignedDoTriplet [lemma, in Stalmarck.complete]
stateAssignedOn [definition, in Stalmarck.complete]
stateAssignedProp1 [lemma, in Stalmarck.complete]
stateAssignedProp2 [lemma, in Stalmarck.complete]
stateDec [library]
stateExtra [library]
stripInRz [definition, in Stalmarck.restrictState]
stripInRzIn [lemma, in Stalmarck.restrictState]
stripInRzIn1 [lemma, in Stalmarck.restrictState]
stripRz [definition, in Stalmarck.interState]
stripRzDec [definition, in Stalmarck.interState]
stripRzDecProp1 [lemma, in Stalmarck.interState]
stripRzDecProp2 [lemma, in Stalmarck.interState]
stripRzDecProp3 [lemma, in Stalmarck.interState]
support [lemma, in Stalmarck.normalize]
supportTriplets [lemma, in Stalmarck.equalBefore]
T
Tautology [definition, in Stalmarck.normalize]TautoRTauto [lemma, in Stalmarck.normalize]
tEval [definition, in Stalmarck.triplet]
Trace [inductive, in Stalmarck.trace]
trace [library]
TraceCorrect [lemma, in Stalmarck.algoTrace]
TraceInList [definition, in Stalmarck.trace]
tRC [constructor, in Stalmarck.makeTriplet]
triple [constructor, in Stalmarck.memoryImplement]
Triple [inductive, in Stalmarck.memoryImplement]
Triplet [constructor, in Stalmarck.triplet]
triplet [inductive, in Stalmarck.triplet]
triplet [library]
tripletDec [definition, in Stalmarck.triplet]
tripletResult [inductive, in Stalmarck.makeTriplet]
tripletTrace [constructor, in Stalmarck.trace]
tripletTraceEval [constructor, in Stalmarck.trace]
tTautology [definition, in Stalmarck.makeTriplet]
t1 [variable, in Stalmarck.algoTrace]
U
unionState [definition, in Stalmarck.unionState]unionState [library]
unionStateAssoc [lemma, in Stalmarck.unionState]
unionStateAssoc1 [lemma, in Stalmarck.unionState]
unionStateEq [lemma, in Stalmarck.unionState]
unionStateInclL [lemma, in Stalmarck.unionState]
unionStateInclR [lemma, in Stalmarck.unionState]
unionStateMin [lemma, in Stalmarck.unionState]
unionStateP [inductive, in Stalmarck.unionState]
unionStatePAssoc2 [lemma, in Stalmarck.unionState]
unionStatePDef [constructor, in Stalmarck.unionState]
unionStatePEq [lemma, in Stalmarck.unionState]
unionStatePEqComp [lemma, in Stalmarck.unionState]
unionStatePIncl [lemma, in Stalmarck.unionState]
unionStatePInclSelf [lemma, in Stalmarck.unionState]
unionStatePRef [lemma, in Stalmarck.unionState]
unionStatePSym [lemma, in Stalmarck.unionState]
unionStatePunionState [lemma, in Stalmarck.unionState]
unionStateSym [lemma, in Stalmarck.unionState]
updateArray [definition, in Stalmarck.addArray]
updateArraya [lemma, in Stalmarck.addArray]
updateArrayb [lemma, in Stalmarck.addArray]
updateArrayInb [lemma, in Stalmarck.addArray]
updateArrayOlist [definition, in Stalmarck.addArray]
updateArrayOtherwise [lemma, in Stalmarck.addArray]
updateArrayPointerDecrease [definition, in Stalmarck.addArray]
updateArrayPointToClassClass [lemma, in Stalmarck.addArray]
updateArrayPointToRef [lemma, in Stalmarck.addArray]
updateCorrect [lemma, in Stalmarck.memoryImplement]
updateEvalNab [lemma, in Stalmarck.memoryImplement]
updateEvalNb [lemma, in Stalmarck.memoryImplement]
updateEvalNO [lemma, in Stalmarck.memoryImplement]
updateEvalN2 [lemma, in Stalmarck.memoryImplement]
updateEvalN2Comp [lemma, in Stalmarck.memoryImplement]
updateEvalZab [lemma, in Stalmarck.memoryImplement]
updateEvalZb [lemma, in Stalmarck.memoryImplement]
updateEvalZO [lemma, in Stalmarck.memoryImplement]
updateEvalZ2 [lemma, in Stalmarck.memoryImplement]
updateEvalZ2Comp [lemma, in Stalmarck.memoryImplement]
updateGetIsClass [lemma, in Stalmarck.addArray]
updatePointToClassClassRef1 [lemma, in Stalmarck.addArray]
updatePointToClassClassRef2 [lemma, in Stalmarck.addArray]
updateWellFormed [lemma, in Stalmarck.addArray]
V
V [constructor, in Stalmarck.normalize]validEquation [definition, in Stalmarck.triplet]
vallStateLe [lemma, in Stalmarck.ltState]
vallStateLt [lemma, in Stalmarck.ltState]
vallStateLtNEq [lemma, in Stalmarck.restrictState]
valRz [definition, in Stalmarck.rZ]
valRzComp [lemma, in Stalmarck.rZ]
valState [definition, in Stalmarck.ltState]
varTriplets [definition, in Stalmarck.triplet]
varTripletsTriplet3 [lemma, in Stalmarck.triplet]
varTripletTriplet1 [lemma, in Stalmarck.triplet]
varTripletTriplet2 [lemma, in Stalmarck.triplet]
varTripletTrue [lemma, in Stalmarck.triplet]
vM [inductive, in Stalmarck.wfArray]
vMDec [definition, in Stalmarck.wfArray]
W
WarCompEq [lemma, in Stalmarck.wfArray]wellFormedArray [inductive, in Stalmarck.wfArray]
wellFormedArrayDef [constructor, in Stalmarck.wfArray]
wellFormedArrayInBothImpEq [lemma, in Stalmarck.wfArray]
wellFormedArrayInImpLt [lemma, in Stalmarck.wfArray]
wellFormedArrayInImpNotEq [lemma, in Stalmarck.wfArray]
wellFormedArrayInImpNotEqSimpl [lemma, in Stalmarck.wfArray]
wellFormedArrayInRzBothImpEq [lemma, in Stalmarck.wfArray]
wellFormedArrayNInImpNotRef [lemma, in Stalmarck.wfArray]
wfArray [section, in Stalmarck.wfArray]
wfArray [library]
wfArray.Ar [variable, in Stalmarck.wfArray]
wfArray.get [variable, in Stalmarck.wfArray]
wfArray.set [variable, in Stalmarck.wfArray]
wfArray.War [variable, in Stalmarck.wfArray]
wfDisjoint [lemma, in Stalmarck.wfArray]
wfOl [lemma, in Stalmarck.wfArray]
wfPcc1 [lemma, in Stalmarck.wfArray]
wfPcc2 [lemma, in Stalmarck.wfArray]
wfPcr [lemma, in Stalmarck.wfArray]
wfPd [lemma, in Stalmarck.wfArray]
Z
zero [definition, in Stalmarck.rZ]zeroInL [lemma, in Stalmarck.restrictState]
Zl1 [variable, in Stalmarck.OrderedListEq_ex]
Zl2 [variable, in Stalmarck.OrderedListEq_ex]
Variable Index
A
A [in Stalmarck.interImplement2_ex]AaddD.a [in Stalmarck.addArray]
AaddD.Ar [in Stalmarck.addArray]
AaddD.b [in Stalmarck.addArray]
AaddD.geta [in Stalmarck.addArray]
AaddD.getb [in Stalmarck.addArray]
AaddD.La [in Stalmarck.addArray]
AaddD.Lb [in Stalmarck.addArray]
AaddD.n [in Stalmarck.addArray]
AaddD.pol [in Stalmarck.addArray]
AaddD.rltab [in Stalmarck.addArray]
AaddD.War [in Stalmarck.addArray]
algos.getT [in Stalmarck.algoDotriplets]
algos.getTCorrect [in Stalmarck.algoDotriplets]
algos.LL [in Stalmarck.algoDotriplets]
appnat [in Stalmarck.OrderedListEq_ex]
appZ [in Stalmarck.OrderedListEq_ex]
Auxrem.A [in Stalmarck.PolyListAux]
Auxrem.ADec [in Stalmarck.PolyListAux]
B
B [in Stalmarck.interImplement2_ex]BP [in Stalmarck.interImplement2_ex]
C
C [in Stalmarck.interImplement2_ex]CP [in Stalmarck.interImplement2_ex]
D
D [in Stalmarck.interImplement2_ex]Deval.Ar [in Stalmarck.memoryImplement]
Deval.War [in Stalmarck.memoryImplement]
DP [in Stalmarck.interImplement2_ex]
Dprop.a [in Stalmarck.memoryImplement]
Dprop.Ar [in Stalmarck.memoryImplement]
Dprop.b [in Stalmarck.memoryImplement]
Dprop.geta [in Stalmarck.memoryImplement]
Dprop.getb [in Stalmarck.memoryImplement]
Dprop.La [in Stalmarck.memoryImplement]
Dprop.Lb [in Stalmarck.memoryImplement]
Dprop.pol [in Stalmarck.memoryImplement]
Dprop.rltab [in Stalmarck.memoryImplement]
Dprop.S [in Stalmarck.memoryImplement]
Dprop.SisAr [in Stalmarck.memoryImplement]
Dprop.War [in Stalmarck.memoryImplement]
d2 [in Stalmarck.interImplement2_ex]
d3 [in Stalmarck.interImplement2_ex]
d4 [in Stalmarck.interImplement2_ex]
E
E [in Stalmarck.interImplement2_ex]EP [in Stalmarck.interImplement2_ex]
G
getminnat [in Stalmarck.OrderedListEq_ex]getminZ [in Stalmarck.OrderedListEq_ex]
I
internat [in Stalmarck.OrderedListEq_ex]interZ [in Stalmarck.OrderedListEq_ex]
L
LB [in Stalmarck.interImplement2_ex]LC [in Stalmarck.interImplement2_ex]
LD [in Stalmarck.interImplement2_ex]
lt.L [in Stalmarck.ltState]
l1 [in Stalmarck.OrderedListEq_ex]
l2 [in Stalmarck.OrderedListEq_ex]
O
odilemma1.getT [in Stalmarck.algoDilemma1]odilemma1.getTCorrect [in Stalmarck.algoDilemma1]
odilemma1.LL [in Stalmarck.algoDilemma1]
odilemma1.n [in Stalmarck.algoDilemma1]
OrderedList.A [in Stalmarck.OrderedListEq]
OrderedList.eqA [in Stalmarck.OrderedListEq]
OrderedList.eqADec' [in Stalmarck.OrderedListEq]
OrderedList.eqARefl [in Stalmarck.OrderedListEq]
OrderedList.eqASym [in Stalmarck.OrderedListEq]
OrderedList.eqATrans [in Stalmarck.OrderedListEq]
OrderedList.f [in Stalmarck.OrderedListEq]
OrderedList.feqA [in Stalmarck.OrderedListEq]
OrderedList.ltA [in Stalmarck.OrderedListEq]
OrderedList.ltAAnti [in Stalmarck.OrderedListEq]
OrderedList.ltADec [in Stalmarck.OrderedListEq]
OrderedList.ltAeqAComp [in Stalmarck.OrderedListEq]
OrderedList.ltAImpNotEqA [in Stalmarck.OrderedListEq]
OrderedList.ltAntiSym [in Stalmarck.OrderedListEq]
OrderedList.ltATrans [in Stalmarck.OrderedListEq]
OrderedList.test [in Stalmarck.OrderedListEq]
OrderedList.testDec [in Stalmarck.OrderedListEq]
OrderedList.testEq [in Stalmarck.OrderedListEq]
orun.t1 [in Stalmarck.algoRun]
orun.t2 [in Stalmarck.algoRun]
ostal.getT [in Stalmarck.algoStalmarck]
ostal.getTCorrect [in Stalmarck.algoStalmarck]
ostal.LL [in Stalmarck.algoStalmarck]
ostal.n [in Stalmarck.algoStalmarck]
R
rA.A [in Stalmarck.rZ]refl.fmap [in Stalmarck.refl]
refl.fmapO [in Stalmarck.refl]
T
t1 [in Stalmarck.algoTrace]W
wfArray.Ar [in Stalmarck.wfArray]wfArray.get [in Stalmarck.wfArray]
wfArray.set [in Stalmarck.wfArray]
wfArray.War [in Stalmarck.wfArray]
Z
Zl1 [in Stalmarck.OrderedListEq_ex]Zl2 [in Stalmarck.OrderedListEq_ex]
Library Index
A
addArrayalgoDilemma1
algoDotriplet
algoDotriplets
algoRun
algoStalmarck
algoTrace
B
BoolAuxC
completeD
doTripletdoTriplets
E
equalBeforeExtract
I
interImplementinterImplement2
interImplement2_ex
interState
L
LetPltState
M
makeTripletmemoryImplement
N
normalizeO
OptionOrderedListEq
OrderedListEq_ex
P
PolyListAuxR
reflrestrictState
rZ
S
sTacticstalmarck
StalTac
StalTac_ex
state
stateDec
stateExtra
T
tracetriplet
U
unionStateW
wfArrayLemma Index
A
addEqComp [in Stalmarck.state]addEqInclState [in Stalmarck.state]
addEqInclState2 [in Stalmarck.state]
addEqMemCorrect [in Stalmarck.memoryImplement]
addEqMem2Correct [in Stalmarck.memoryImplement]
addEqUnion [in Stalmarck.unionState]
addInterAuxProp [in Stalmarck.interImplement2]
andSym [in Stalmarck.restrictState]
appendCom [in Stalmarck.OrderedListEq]
appendDisjIncl1 [in Stalmarck.OrderedListEq]
appendDisjIncl2 [in Stalmarck.OrderedListEq]
appendDisjoint [in Stalmarck.OrderedListEq]
appendEqInv [in Stalmarck.OrderedListEq]
appendfAppend [in Stalmarck.OrderedListEq]
appendfDisjoint [in Stalmarck.OrderedListEq]
appendfInclEq1 [in Stalmarck.OrderedListEq]
appendfInclEq2 [in Stalmarck.OrderedListEq]
appendfIncl1 [in Stalmarck.OrderedListEq]
appendfIncl2 [in Stalmarck.OrderedListEq]
appendfInv [in Stalmarck.OrderedListEq]
appendfInvEq [in Stalmarck.OrderedListEq]
appendfOlist [in Stalmarck.OrderedListEq]
appendIncl1 [in Stalmarck.OrderedListEq]
appendIncl2 [in Stalmarck.OrderedListEq]
appendInv [in Stalmarck.OrderedListEq]
appendOlist [in Stalmarck.OrderedListEq]
appendSup [in Stalmarck.OrderedListEq]
appTraceCorrect [in Stalmarck.algoDotriplets]
C
checkTrace [in Stalmarck.algoTrace]CompInterR [in Stalmarck.interState]
contradictoryAddEq [in Stalmarck.restrictState]
contradictoryEq [in Stalmarck.algoDotriplet]
contradictoryNotRealize [in Stalmarck.state]
Contradict1 [in Stalmarck.sTactic]
Contradict2 [in Stalmarck.sTactic]
Contradict3 [in Stalmarck.sTactic]
ContrIncl [in Stalmarck.state]
ContrInterL [in Stalmarck.interState]
ContrInterR [in Stalmarck.interState]
c2 [in Stalmarck.StalTac_ex]
D
de_morgan4 [in Stalmarck.BoolAux]de_morgan3 [in Stalmarck.BoolAux]
de_morgan2 [in Stalmarck.BoolAux]
de_morgan1 [in Stalmarck.BoolAux]
diffElemNone [in Stalmarck.OrderedListEq]
diffElemSomeIn [in Stalmarck.OrderedListEq]
diffElemSomeNIn [in Stalmarck.OrderedListEq]
DilemmaContrad [in Stalmarck.complete]
DilemmaContradAux [in Stalmarck.complete]
dilemmaNCorrect [in Stalmarck.algoDilemma1]
dilemma1Correct [in Stalmarck.algoDilemma1]
dilemma1RCorrect [in Stalmarck.algoDilemma1]
dilemma1RRCorrect [in Stalmarck.algoDilemma1]
dilemma1RRLCorrect [in Stalmarck.algoDilemma1]
DisjbLb [in Stalmarck.addArray]
DisjLaLc [in Stalmarck.addArray]
DisjointCom [in Stalmarck.OrderedListEq]
DisjointCons1 [in Stalmarck.OrderedListEq]
DisjointCons2 [in Stalmarck.OrderedListEq]
Disjointf [in Stalmarck.OrderedListEq]
DisjointIncl [in Stalmarck.OrderedListEq]
DisjointInclL [in Stalmarck.OrderedListEq]
DisjointInclR [in Stalmarck.OrderedListEq]
DisjointInv1 [in Stalmarck.OrderedListEq]
DisjointInv2 [in Stalmarck.OrderedListEq]
doTripletBisIncl [in Stalmarck.doTriplet]
doTripletConfl [in Stalmarck.doTriplet]
doTripletConflEx [in Stalmarck.doTriplet]
doTripletCongruent [in Stalmarck.doTriplets]
doTripletCongruentEx [in Stalmarck.doTriplet]
doTripletEq [in Stalmarck.doTriplet]
doTripletEqAux1 [in Stalmarck.doTriplet]
doTripletEqAux2 [in Stalmarck.doTriplet]
doTripletEqComp [in Stalmarck.doTriplet]
doTripletEqCompEx [in Stalmarck.doTriplet]
doTripletEqMonotone [in Stalmarck.doTriplet]
doTripletFCorrect [in Stalmarck.algoDotriplet]
doTripletFsCorrect [in Stalmarck.algoDotriplets]
doTripletFsNCorrect [in Stalmarck.algoDotriplets]
doTripletFsRCorrect [in Stalmarck.algoDotriplets]
doTripletIncl [in Stalmarck.doTriplet]
doTripletInvol [in Stalmarck.doTriplet]
doTripletInvolEx [in Stalmarck.doTriplet]
doTripletInvolExAux1 [in Stalmarck.doTriplet]
doTripletInvolExAux2 [in Stalmarck.doTriplet]
doTripletMonotoneEx [in Stalmarck.doTriplet]
doTripletRestrict [in Stalmarck.restrictState]
doTripletRestrictAux1 [in Stalmarck.restrictState]
doTripletRestrictAux2 [in Stalmarck.restrictState]
doTripletRestrictInv [in Stalmarck.restrictState]
doTripletsComp [in Stalmarck.doTriplets]
doTripletsConftEx [in Stalmarck.doTriplets]
doTripletsExTrace [in Stalmarck.trace]
doTripletsIncl [in Stalmarck.doTriplets]
doTripletsInclList [in Stalmarck.doTriplets]
doTripletsMonotoneEx [in Stalmarck.doTriplets]
doTripletsRealizeStateEval [in Stalmarck.doTriplets]
doTripletsRestrict [in Stalmarck.restrictState]
doTripletsRestrictBis [in Stalmarck.restrictState]
doTripletsRestrictInv [in Stalmarck.restrictState]
doTripletsRTrans [in Stalmarck.doTriplets]
doTripletsTermEx [in Stalmarck.doTriplets]
doTripletsTermExAux [in Stalmarck.doTriplets]
doTripletsUnionEx [in Stalmarck.doTriplets]
doTripletUnionAux1 [in Stalmarck.doTriplet]
doTripletUnionAux2 [in Stalmarck.doTriplet]
doTripletUnionEx [in Stalmarck.doTriplet]
doTripletUnionEx1 [in Stalmarck.doTriplet]
doTripletUnionEx2 [in Stalmarck.doTriplet]
dTCorrect [in Stalmarck.algoDilemma1]
dubois20 [in Stalmarck.StalTac_ex]
E
EqboolDec [in Stalmarck.stateExtra]eqb_com [in Stalmarck.BoolAux]
eqb_false_b [in Stalmarck.BoolAux]
eqb_b_false [in Stalmarck.BoolAux]
eqb_b_true [in Stalmarck.BoolAux]
eqb_true_b [in Stalmarck.BoolAux]
eqConstrStateCons [in Stalmarck.stateDec]
eqConstrStateContrGen [in Stalmarck.stateDec]
eqConstrStateImpeqStateRz [in Stalmarck.stateDec]
eqConstrStateIn [in Stalmarck.stateDec]
eqConstrStateInDouble [in Stalmarck.interState]
eqConstrStateInL [in Stalmarck.interState]
eqConstrStateInR [in Stalmarck.interState]
eqConstrStateInv [in Stalmarck.stateDec]
eqConstrStateRef [in Stalmarck.stateDec]
eqConstrStateSimpl [in Stalmarck.stateDec]
eqConstrStateSym [in Stalmarck.stateDec]
eqConstrStateTrans [in Stalmarck.stateDec]
eqConstrStateTransConstr [in Stalmarck.stateDec]
EqLInv [in Stalmarck.OrderedListEq]
EqLOlist [in Stalmarck.OrderedListEq]
EqLRef [in Stalmarck.OrderedListEq]
EqLTrans [in Stalmarck.OrderedListEq]
eqNotltRz [in Stalmarck.interImplement]
EqrZComp [in Stalmarck.memoryImplement]
eqRzComp [in Stalmarck.rZ]
eqRzElim [in Stalmarck.triplet]
eqrZRefl [in Stalmarck.rZ]
eqrZSym [in Stalmarck.rZ]
eqrZTrans [in Stalmarck.rZ]
eqStateAddEq [in Stalmarck.state]
eqStateaddEq1 [in Stalmarck.state]
eqStateaddEq2 [in Stalmarck.state]
eqStateContr [in Stalmarck.state]
eqStateContrSimpl1 [in Stalmarck.state]
eqStateEq [in Stalmarck.state]
eqStateEqEvalZ [in Stalmarck.algoDotriplet]
eqStateEq1 [in Stalmarck.algoDotriplet]
eqStateEq2 [in Stalmarck.algoDotriplet]
eqStateEq2EvalZ [in Stalmarck.algoDotriplet]
eqStateEvalZ [in Stalmarck.algoDotriplet]
eqStateIncl [in Stalmarck.state]
eqStateInv [in Stalmarck.state]
eqStateInvInv [in Stalmarck.state]
eqStateRarray [in Stalmarck.algoDotriplets]
eqStateRef [in Stalmarck.state]
eqStateRzPImpeqConstrState [in Stalmarck.stateDec]
eqStateRzTail [in Stalmarck.stateDec]
eqStateSym [in Stalmarck.state]
eqStateTrans [in Stalmarck.state]
equalBeforeElim [in Stalmarck.equalBefore]
equalBeforeExtend [in Stalmarck.equalBefore]
equalBeforeLt [in Stalmarck.equalBefore]
equalBeforeMakeTriplets [in Stalmarck.makeTriplet]
equalBeforeMakeTripletsFun [in Stalmarck.makeTriplet]
equalBeforeNext [in Stalmarck.equalBefore]
equalBeforeREval [in Stalmarck.equalBefore]
equalBeforerZEval [in Stalmarck.equalBefore]
equalBeforeSym [in Stalmarck.equalBefore]
equalBeforeTEval [in Stalmarck.equalBefore]
equalBeforeTrans [in Stalmarck.equalBefore]
evalNEvalZ [in Stalmarck.memoryImplement]
evalRealizeState [in Stalmarck.doTriplet]
evalRealizeStateAux1 [in Stalmarck.doTriplet]
evalRealizeStateAux2 [in Stalmarck.doTriplet]
evalTraceComp [in Stalmarck.trace]
evalTraceEq [in Stalmarck.algoDotriplets]
evalTraceEq [in Stalmarck.trace]
evalZComp [in Stalmarck.memoryImplement]
evalZFalse [in Stalmarck.memoryImplement]
evalZInv [in Stalmarck.memoryImplement]
evalZltOr [in Stalmarck.memoryImplement]
evalZMin [in Stalmarck.interImplement]
evalZMin [in Stalmarck.memoryImplement]
evalZTrue [in Stalmarck.memoryImplement]
ExprToPropF [in Stalmarck.refl]
ExprToPropF2 [in Stalmarck.refl]
ExprToPropTautology [in Stalmarck.refl]
extendEvalMakeTriplets [in Stalmarck.makeTriplet]
extendEvalMakeTripletsFun [in Stalmarck.makeTriplet]
extendFunrZEval [in Stalmarck.equalBefore]
extendFunrZEvalExact [in Stalmarck.equalBefore]
F
fappendfAppend [in Stalmarck.OrderedListEq]fappendfDisjoint [in Stalmarck.OrderedListEq]
fappendfInclEq1 [in Stalmarck.OrderedListEq]
fappendfInclEq2 [in Stalmarck.OrderedListEq]
fappendfIncl1 [in Stalmarck.OrderedListEq]
fappendfIncl2 [in Stalmarck.OrderedListEq]
fappendfInv [in Stalmarck.OrderedListEq]
fappendfInvEq [in Stalmarck.OrderedListEq]
fappendfOlist [in Stalmarck.OrderedListEq]
fInTCorrect [in Stalmarck.algoTrace]
forallgetEquivgetRzMin [in Stalmarck.interImplement]
FStalCorrectComp [in Stalmarck.algoDotriplets]
FStalCorrectIncl [in Stalmarck.algoDotriplets]
FStalCorrect0 [in Stalmarck.algoDotriplets]
F1 [in Stalmarck.algoRun]
F2 [in Stalmarck.algoRun]
F3 [in Stalmarck.algoRun]
G
geMinIn [in Stalmarck.OrderedListEq]GetClassNProp [in Stalmarck.memoryImplement]
getClassOlist [in Stalmarck.memoryImplement]
getEquivIdL [in Stalmarck.interImplement]
getEquivIdR [in Stalmarck.interImplement]
getEquivInter [in Stalmarck.interImplement]
getEquivListProp1 [in Stalmarck.interImplement]
getEquivListProp2 [in Stalmarck.interImplement]
getEquivListProp3 [in Stalmarck.interImplement]
getEquivListProp4 [in Stalmarck.interImplement]
getEquivMinEq1 [in Stalmarck.interImplement]
getEquivMinEq2 [in Stalmarck.interImplement]
getEquivMinIn1 [in Stalmarck.interImplement]
getEquivMinIn2 [in Stalmarck.interImplement]
getEquivMinMin [in Stalmarck.interImplement]
getEquivMinMinEq [in Stalmarck.interImplement]
getEquivMinSym [in Stalmarck.interImplement]
getEquivProp1 [in Stalmarck.interImplement]
getEquivProp2 [in Stalmarck.interImplement]
getEquivProp3 [in Stalmarck.interImplement]
getMinComp [in Stalmarck.OrderedListEq]
getMinIdSym [in Stalmarck.interImplement]
getMinInvInd [in Stalmarck.interImplement]
getMinInvSym [in Stalmarck.interImplement]
getMinMin [in Stalmarck.OrderedListEq]
getMinNone [in Stalmarck.OrderedListEq]
getNotIdP [in Stalmarck.wfArray]
getRzMinEq1 [in Stalmarck.interImplement]
getRzMinEq2 [in Stalmarck.interImplement]
getRzMinIn1 [in Stalmarck.interImplement]
getRzMinIn2 [in Stalmarck.interImplement]
getRzMinMin [in Stalmarck.interImplement]
getRzMinMinEq [in Stalmarck.interImplement]
getRzMinSym [in Stalmarck.interImplement]
getRzMinUnique [in Stalmarck.interImplement]
getTCorrect [in Stalmarck.algoTrace]
I
implb_elim [in Stalmarck.BoolAux]implb_false_b [in Stalmarck.BoolAux]
implb_true_b [in Stalmarck.BoolAux]
implb_b_false [in Stalmarck.BoolAux]
implb_b_true [in Stalmarck.BoolAux]
InclEqCons [in Stalmarck.OrderedListEq]
InclEqNil [in Stalmarck.OrderedListEq]
InclEqOlist [in Stalmarck.OrderedListEq]
InclEqRef [in Stalmarck.OrderedListEq]
InclEqTrans [in Stalmarck.OrderedListEq]
inclImpImplEq [in Stalmarck.OrderedListEq]
inclStateAddEq [in Stalmarck.state]
inclStateAddEqInv [in Stalmarck.state]
inclStateEqStateComp [in Stalmarck.state]
inclStateIn [in Stalmarck.state]
inclStateRef [in Stalmarck.state]
inclStateTrans [in Stalmarck.state]
InEqComp [in Stalmarck.OrderedListEq]
InEqInv [in Stalmarck.wfArray]
InEqNList [in Stalmarck.OrderedListEq]
InEqOlistInv [in Stalmarck.OrderedListEq]
InEqSup [in Stalmarck.OrderedListEq]
inImpInEq [in Stalmarck.OrderedListEq]
initCorrect [in Stalmarck.memoryImplement]
inLt [in Stalmarck.equalBefore]
inMapComp [in Stalmarck.interImplement]
InRestrictState [in Stalmarck.restrictState]
InRzDec [in Stalmarck.wfArray]
InState [in Stalmarck.restrictState]
interAssoc [in Stalmarck.interState]
interCom [in Stalmarck.OrderedListEq]
interfCom [in Stalmarck.OrderedListEq]
interfIncl1 [in Stalmarck.OrderedListEq]
interfIncl2 [in Stalmarck.OrderedListEq]
interfMin [in Stalmarck.OrderedListEq]
interfOlist [in Stalmarck.OrderedListEq]
interfProp1 [in Stalmarck.OrderedListEq]
interIncl1 [in Stalmarck.OrderedListEq]
interIncl2 [in Stalmarck.OrderedListEq]
interMemEqStateRz [in Stalmarck.interState]
interMemInL [in Stalmarck.interState]
interMemInR [in Stalmarck.interState]
interMemMin [in Stalmarck.interState]
interMemProp [in Stalmarck.interState]
interMin [in Stalmarck.OrderedListEq]
interOlist [in Stalmarck.OrderedListEq]
interStateEq [in Stalmarck.interState]
interStatePEq [in Stalmarck.interState]
interStatePIncl [in Stalmarck.interState]
interStatePInclSelf [in Stalmarck.interState]
interStatePRef [in Stalmarck.interState]
interStatePSym [in Stalmarck.interState]
interStateSym [in Stalmarck.interState]
interSup [in Stalmarck.OrderedListEq]
inTripletsComp [in Stalmarck.triplet]
inTripletsCompInv [in Stalmarck.triplet]
inTripletsFalse [in Stalmarck.triplet]
inTripletsIn [in Stalmarck.triplet]
inTripletsTrue [in Stalmarck.triplet]
inTripletsVarTriplet [in Stalmarck.triplet]
L
lePlusComp [in Stalmarck.ltState]ltlePlusCompL [in Stalmarck.ltState]
ltlePlusCompR [in Stalmarck.ltState]
ltStateEqComp [in Stalmarck.ltState]
ltStateLt [in Stalmarck.ltState]
ltStateTrans [in Stalmarck.ltState]
ltStateWf [in Stalmarck.ltState]
M
makeTripletsFunIncl [in Stalmarck.makeTriplet]makeTripletsFunIncr [in Stalmarck.makeTriplet]
makeTripletsFunMax [in Stalmarck.makeTriplet]
makeTripletsIn [in Stalmarck.makeTriplet]
map_id [in Stalmarck.PolyListAux]
maxProp1 [in Stalmarck.rZ]
maxProp2 [in Stalmarck.rZ]
maxProp3 [in Stalmarck.rZ]
maxProp4 [in Stalmarck.rZ]
maxProp5 [in Stalmarck.rZ]
maxProp6 [in Stalmarck.rZ]
maxVarTripletsRlt [in Stalmarck.makeTriplet]
minProp1 [in Stalmarck.rZ]
minProp2 [in Stalmarck.rZ]
minProp3 [in Stalmarck.rZ]
minProp4 [in Stalmarck.rZ]
minProp5 [in Stalmarck.rZ]
minProp6 [in Stalmarck.rZ]
N
NcountLe [in Stalmarck.ltState]NcountLt [in Stalmarck.ltState]
negbElim [in Stalmarck.stateExtra]
negRealizeTriplets [in Stalmarck.complete]
normEval [in Stalmarck.normalize]
normImplEval [in Stalmarck.normalize]
normNotEval [in Stalmarck.normalize]
normOrEval [in Stalmarck.normalize]
NotEqComp [in Stalmarck.rZ]
NotInAppendf [in Stalmarck.OrderedListEq]
NotInCons1 [in Stalmarck.PolyListAux]
NotInEqComp [in Stalmarck.OrderedListEq]
notrltzero [in Stalmarck.memoryImplement]
NrelLe [in Stalmarck.ltState]
NrelLt [in Stalmarck.ltState]
nthTailProp1 [in Stalmarck.complete]
nthTailProp2 [in Stalmarck.complete]
nthTailProp3 [in Stalmarck.complete]
O
Olistf [in Stalmarck.OrderedListEq]OlistIn [in Stalmarck.OrderedListEq]
OlistInv [in Stalmarck.OrderedListEq]
OlistSkip [in Stalmarck.OrderedListEq]
OlistSup [in Stalmarck.OrderedListEq]
OlistSupEq [in Stalmarck.OrderedListEq]
OlistUnique [in Stalmarck.OrderedListEq]
OlistUniqueEq [in Stalmarck.OrderedListEq]
oneStateAllLe [in Stalmarck.ltState]
oneStateAllLt [in Stalmarck.ltState]
oneStateLe [in Stalmarck.ltState]
oneStateLt [in Stalmarck.ltState]
orb_false_2 [in Stalmarck.BoolAux]
orb_false_1 [in Stalmarck.BoolAux]
P
Praeclarum [in Stalmarck.StalTac_ex]prodRzInL [in Stalmarck.restrictState]
prodRzInR [in Stalmarck.restrictState]
prodRzProp [in Stalmarck.interState]
puz002_1 [in Stalmarck.StalTac_ex]
puz003_1 [in Stalmarck.StalTac_ex]
R
rArrayContradictory [in Stalmarck.interImplement2]rArrayDef [in Stalmarck.rZ]
rArrayDefP [in Stalmarck.refl]
rArrayDef1 [in Stalmarck.rZ]
rArrayDef1P [in Stalmarck.refl]
rArrayDef2 [in Stalmarck.rZ]
rArrayDef2P [in Stalmarck.refl]
rArrayGetEvalN [in Stalmarck.memoryImplement]
rArrayGetEvalZ [in Stalmarck.memoryImplement]
rArraySetListInv1 [in Stalmarck.addArray]
rArraySetListInv2 [in Stalmarck.addArray]
rArrayStateDef1 [in Stalmarck.memoryImplement]
rArrayStateDef2 [in Stalmarck.memoryImplement]
rArrayStateEqState [in Stalmarck.memoryImplement]
rArrayStateGet [in Stalmarck.memoryImplement]
Realizable [in Stalmarck.stateExtra]
RealizableAux1 [in Stalmarck.stateExtra]
RealizableAux2 [in Stalmarck.stateExtra]
RealizableAux3 [in Stalmarck.stateExtra]
RealizableCstr [in Stalmarck.stateExtra]
Realizable2 [in Stalmarck.stateExtra]
RealizeNegb [in Stalmarck.stateExtra]
realizeStateAddEq [in Stalmarck.state]
realizeStateEval [in Stalmarck.doTriplet]
realizeStateEvalAux1 [in Stalmarck.doTriplet]
realizeStateEvalAux2 [in Stalmarck.doTriplet]
realizeStateEvalEquiv [in Stalmarck.doTriplet]
realizeStateIncl [in Stalmarck.state]
realizeStateInclInv [in Stalmarck.stateExtra]
realizeStateInv [in Stalmarck.state]
realizeStateInvAddEq [in Stalmarck.state]
realizeStateInvAddEq2 [in Stalmarck.state]
realizeStateInvComp [in Stalmarck.state]
realizeStateNil [in Stalmarck.state]
realizeTripletCons [in Stalmarck.triplet]
realizeTripletIncl [in Stalmarck.triplet]
realizeTripletNil [in Stalmarck.triplet]
refSameEq [in Stalmarck.wfArray]
remEq [in Stalmarck.PolyListAux]
remIn [in Stalmarck.PolyListAux]
remNotIn [in Stalmarck.PolyListAux]
remSizeLess [in Stalmarck.PolyListAux]
restricMonotone [in Stalmarck.restrictState]
RestrictAddEq [in Stalmarck.restrictState]
RestrictAddEq1 [in Stalmarck.restrictState]
RestrictAddEq2 [in Stalmarck.restrictState]
restrictContradiction [in Stalmarck.restrictState]
restrictDoTripletComp [in Stalmarck.restrictState]
restrictDoTripletCompAux1 [in Stalmarck.restrictState]
restrictDoTripletCompAux2 [in Stalmarck.restrictState]
restrictDoTripletsComp [in Stalmarck.restrictState]
restrictDoTripletsCompAux1 [in Stalmarck.restrictState]
restrictEqComp [in Stalmarck.restrictState]
restrictStateComp [in Stalmarck.restrictState]
restrictStateIncl [in Stalmarck.restrictState]
restrictStateInvol [in Stalmarck.restrictState]
restrictStateInZeroL [in Stalmarck.restrictState]
restrictStateInZeroR [in Stalmarck.restrictState]
ResTripletInResTriplets [in Stalmarck.restrictState]
rIwF [in Stalmarck.algoTrace]
rltAntiSym [in Stalmarck.rZ]
rltDef2 [in Stalmarck.rZ]
rltNotRefl [in Stalmarck.rZ]
rltRmaxLeft [in Stalmarck.rZ]
rltRmaxRight [in Stalmarck.rZ]
rltRnext2Inv [in Stalmarck.rZ]
rltTrans [in Stalmarck.rZ]
rltTransRnext1 [in Stalmarck.rZ]
rltTransRnext2 [in Stalmarck.rZ]
rmaxRlt [in Stalmarck.rZ]
rmaxRltLeft [in Stalmarck.rZ]
rmaxRltRight [in Stalmarck.rZ]
rNextInv [in Stalmarck.rZ]
rnextMono [in Stalmarck.rZ]
rnextNotZero [in Stalmarck.rZ]
rnextRlt [in Stalmarck.rZ]
rNextS [in Stalmarck.rZ]
rTautotTauto [in Stalmarck.makeTriplet]
rTreeDef1 [in Stalmarck.rZ]
rTreeDef1P [in Stalmarck.refl]
rTreeDef2 [in Stalmarck.rZ]
rTreeDef2 [in Stalmarck.refl]
runC [in Stalmarck.algoRun]
runCorrect [in Stalmarck.algoRun]
rVltrZComp [in Stalmarck.rZ]
rZCompEq [in Stalmarck.rZ]
rZCompInv [in Stalmarck.rZ]
rZCompInvol [in Stalmarck.rZ]
rZCompInvolList [in Stalmarck.interImplement]
rZEvalCompInv [in Stalmarck.state]
rZEvalEvalRZMakeTriplets [in Stalmarck.makeTriplet]
rZEvalREvalMakeTriplets [in Stalmarck.makeTriplet]
rZltAntiSym [in Stalmarck.rZ]
rZltDef2 [in Stalmarck.rZ]
rZltEqComp [in Stalmarck.rZ]
rZltNotRefl [in Stalmarck.rZ]
rZltTrans [in Stalmarck.rZ]
S
samePolRzComp [in Stalmarck.rZ]samePolRzEqRz [in Stalmarck.rZ]
samePolRzInvRvlt [in Stalmarck.rZ]
samePolRzRvlt [in Stalmarck.rZ]
samePolRzsamePolRz [in Stalmarck.rZ]
samePolRzValRz [in Stalmarck.rZ]
samePolSamePolRz [in Stalmarck.rZ]
SomeComp [in Stalmarck.Option]
stalCorrect [in Stalmarck.algoStalmarck]
stalmarckComp [in Stalmarck.stalmarck]
stalmarckComplete [in Stalmarck.complete]
stalmarckCorrect [in Stalmarck.stalmarck]
stalmarckExTrace [in Stalmarck.trace]
stalmarckGivesValidEquation [in Stalmarck.stalmarck]
stalmarckIncl [in Stalmarck.stalmarck]
stalmarckInclList [in Stalmarck.algoDotriplets]
stalmarckMonotoneEx [in Stalmarck.stalmarck]
stalmarckRealizeStateEval [in Stalmarck.stalmarck]
stalmarckUnionEx [in Stalmarck.stalmarck]
stalNCorrect [in Stalmarck.algoStalmarck]
stateAssignContrad [in Stalmarck.complete]
stateAssignedDoTriplet [in Stalmarck.complete]
stateAssignedProp1 [in Stalmarck.complete]
stateAssignedProp2 [in Stalmarck.complete]
stripInRzIn [in Stalmarck.restrictState]
stripInRzIn1 [in Stalmarck.restrictState]
stripRzDecProp1 [in Stalmarck.interState]
stripRzDecProp2 [in Stalmarck.interState]
stripRzDecProp3 [in Stalmarck.interState]
support [in Stalmarck.normalize]
supportTriplets [in Stalmarck.equalBefore]
T
TautoRTauto [in Stalmarck.normalize]TraceCorrect [in Stalmarck.algoTrace]
U
unionStateAssoc [in Stalmarck.unionState]unionStateAssoc1 [in Stalmarck.unionState]
unionStateEq [in Stalmarck.unionState]
unionStateInclL [in Stalmarck.unionState]
unionStateInclR [in Stalmarck.unionState]
unionStateMin [in Stalmarck.unionState]
unionStatePAssoc2 [in Stalmarck.unionState]
unionStatePEq [in Stalmarck.unionState]
unionStatePEqComp [in Stalmarck.unionState]
unionStatePIncl [in Stalmarck.unionState]
unionStatePInclSelf [in Stalmarck.unionState]
unionStatePRef [in Stalmarck.unionState]
unionStatePSym [in Stalmarck.unionState]
unionStatePunionState [in Stalmarck.unionState]
unionStateSym [in Stalmarck.unionState]
updateArraya [in Stalmarck.addArray]
updateArrayb [in Stalmarck.addArray]
updateArrayInb [in Stalmarck.addArray]
updateArrayOtherwise [in Stalmarck.addArray]
updateArrayPointToClassClass [in Stalmarck.addArray]
updateArrayPointToRef [in Stalmarck.addArray]
updateCorrect [in Stalmarck.memoryImplement]
updateEvalNab [in Stalmarck.memoryImplement]
updateEvalNb [in Stalmarck.memoryImplement]
updateEvalNO [in Stalmarck.memoryImplement]
updateEvalN2 [in Stalmarck.memoryImplement]
updateEvalN2Comp [in Stalmarck.memoryImplement]
updateEvalZab [in Stalmarck.memoryImplement]
updateEvalZb [in Stalmarck.memoryImplement]
updateEvalZO [in Stalmarck.memoryImplement]
updateEvalZ2 [in Stalmarck.memoryImplement]
updateEvalZ2Comp [in Stalmarck.memoryImplement]
updateGetIsClass [in Stalmarck.addArray]
updatePointToClassClassRef1 [in Stalmarck.addArray]
updatePointToClassClassRef2 [in Stalmarck.addArray]
updateWellFormed [in Stalmarck.addArray]
V
vallStateLe [in Stalmarck.ltState]vallStateLt [in Stalmarck.ltState]
vallStateLtNEq [in Stalmarck.restrictState]
valRzComp [in Stalmarck.rZ]
varTripletsTriplet3 [in Stalmarck.triplet]
varTripletTriplet1 [in Stalmarck.triplet]
varTripletTriplet2 [in Stalmarck.triplet]
varTripletTrue [in Stalmarck.triplet]
W
WarCompEq [in Stalmarck.wfArray]wellFormedArrayInBothImpEq [in Stalmarck.wfArray]
wellFormedArrayInImpLt [in Stalmarck.wfArray]
wellFormedArrayInImpNotEq [in Stalmarck.wfArray]
wellFormedArrayInImpNotEqSimpl [in Stalmarck.wfArray]
wellFormedArrayInRzBothImpEq [in Stalmarck.wfArray]
wellFormedArrayNInImpNotRef [in Stalmarck.wfArray]
wfDisjoint [in Stalmarck.wfArray]
wfOl [in Stalmarck.wfArray]
wfPcc1 [in Stalmarck.wfArray]
wfPcc2 [in Stalmarck.wfArray]
wfPcr [in Stalmarck.wfArray]
wfPd [in Stalmarck.wfArray]
Z
zeroInL [in Stalmarck.restrictState]Constructor Index
A
ANd [in Stalmarck.normalize]appendEqA [in Stalmarck.OrderedListEq]
appendLtA1 [in Stalmarck.OrderedListEq]
appendLtA2 [in Stalmarck.OrderedListEq]
appendNil1 [in Stalmarck.OrderedListEq]
appendNil2 [in Stalmarck.OrderedListEq]
C
class [in Stalmarck.wfArray]D
dilemmaTrace [in Stalmarck.trace]dilemmaTraceEval [in Stalmarck.trace]
DisjointDef [in Stalmarck.OrderedListEq]
doTripletAndPpmq [in Stalmarck.doTriplet]
doTripletAndPpmr [in Stalmarck.doTriplet]
doTripletAndPpT [in Stalmarck.doTriplet]
doTripletAndPqF [in Stalmarck.doTriplet]
doTripletAndPqmr [in Stalmarck.doTriplet]
doTripletAndPqr [in Stalmarck.doTriplet]
doTripletAndPqT [in Stalmarck.doTriplet]
doTripletAndPrF [in Stalmarck.doTriplet]
doTripletAndPrT [in Stalmarck.doTriplet]
doTripletEqPpF [in Stalmarck.doTriplet]
doTripletEqPpmq [in Stalmarck.doTriplet]
doTripletEqPpmr [in Stalmarck.doTriplet]
doTripletEqPpq [in Stalmarck.doTriplet]
doTripletEqPpr [in Stalmarck.doTriplet]
doTripletEqPpT [in Stalmarck.doTriplet]
doTripletEqPqF [in Stalmarck.doTriplet]
doTripletEqPqmr [in Stalmarck.doTriplet]
doTripletEqPqr [in Stalmarck.doTriplet]
doTripletEqPqT [in Stalmarck.doTriplet]
doTripletEqPrF [in Stalmarck.doTriplet]
doTripletEqPrT [in Stalmarck.doTriplet]
doTripletsRef [in Stalmarck.doTriplets]
doTripletsTrans [in Stalmarck.doTriplets]
E
emptyTrace [in Stalmarck.trace]emptyTraceEval [in Stalmarck.trace]
Eq [in Stalmarck.normalize]
eqConstrStateComp1 [in Stalmarck.stateDec]
eqConstrStateComp2 [in Stalmarck.stateDec]
eqConstrStateComp3 [in Stalmarck.stateDec]
eqConstrStateComp4 [in Stalmarck.stateDec]
eqConstrStateContr [in Stalmarck.stateDec]
eqConstrStateNil [in Stalmarck.stateDec]
eqConstrStateTail [in Stalmarck.stateDec]
EqLCons [in Stalmarck.OrderedListEq]
EqLNil [in Stalmarck.OrderedListEq]
eqOptionNone [in Stalmarck.Option]
eqOptionSome [in Stalmarck.Option]
eqStateRzContr [in Stalmarck.state]
eqStateRzIn [in Stalmarck.state]
eqStateRzInv [in Stalmarck.state]
eqStateRzRef [in Stalmarck.state]
eqStateRzSym [in Stalmarck.state]
eqStateRzTrans [in Stalmarck.state]
I
Impl [in Stalmarck.normalize]InclEqDef [in Stalmarck.OrderedListEq]
InEqHead [in Stalmarck.OrderedListEq]
InEqSkip [in Stalmarck.OrderedListEq]
inN [in Stalmarck.refl]
inNodeLeft [in Stalmarck.refl]
inNodeRight [in Stalmarck.refl]
inRN [in Stalmarck.normalize]
inRNodeLeft [in Stalmarck.normalize]
inRNodeRight [in Stalmarck.normalize]
inRV [in Stalmarck.normalize]
interEqA [in Stalmarck.OrderedListEq]
interLtA1 [in Stalmarck.OrderedListEq]
interLtA2 [in Stalmarck.OrderedListEq]
interNil1 [in Stalmarck.OrderedListEq]
interNil2 [in Stalmarck.OrderedListEq]
inV [in Stalmarck.refl]
N
N [in Stalmarck.normalize]Node [in Stalmarck.normalize]
None [in Stalmarck.Option]
O
OlistArrayDef [in Stalmarck.wfArray]OlistCons [in Stalmarck.OrderedListEq]
OlistNil [in Stalmarck.OrderedListEq]
OlistOne [in Stalmarck.OrderedListEq]
Or [in Stalmarck.normalize]
P
PNone [in Stalmarck.refl]pointerDecreaseDef [in Stalmarck.wfArray]
pointToClassClassRef [in Stalmarck.wfArray]
pointToClassRefDef [in Stalmarck.wfArray]
PSome [in Stalmarck.refl]
Q
quatuor [in Stalmarck.algoDotriplets]R
rAnd [in Stalmarck.normalize]rArrayMake [in Stalmarck.rZ]
rArrayMakeP [in Stalmarck.refl]
ref [in Stalmarck.wfArray]
rEmpty [in Stalmarck.rZ]
rEmptyP [in Stalmarck.refl]
rEq [in Stalmarck.normalize]
rN [in Stalmarck.normalize]
rNode [in Stalmarck.normalize]
rSplit [in Stalmarck.rZ]
rSplitP [in Stalmarck.refl]
rV [in Stalmarck.normalize]
rZMinus [in Stalmarck.rZ]
rZPlus [in Stalmarck.rZ]
S
seqTrace [in Stalmarck.trace]seqTraceEval [in Stalmarck.trace]
Some [in Stalmarck.Option]
stalmarckPref [in Stalmarck.stalmarck]
stalmarckPSplit [in Stalmarck.stalmarck]
stalmarckTrans [in Stalmarck.stalmarck]
T
tRC [in Stalmarck.makeTriplet]triple [in Stalmarck.memoryImplement]
Triplet [in Stalmarck.triplet]
tripletTrace [in Stalmarck.trace]
tripletTraceEval [in Stalmarck.trace]
U
unionStatePDef [in Stalmarck.unionState]V
V [in Stalmarck.normalize]W
wellFormedArrayDef [in Stalmarck.wfArray]Inductive Index
A
append [in Stalmarck.OrderedListEq]B
boolOp [in Stalmarck.normalize]D
Disjoint [in Stalmarck.OrderedListEq]doTripletP [in Stalmarck.doTriplet]
doTripletsP [in Stalmarck.doTriplets]
E
eqConstrState [in Stalmarck.stateDec]EqL [in Stalmarck.OrderedListEq]
eqOption [in Stalmarck.Option]
eqStateRz [in Stalmarck.state]
evalTrace [in Stalmarck.trace]
Expr [in Stalmarck.normalize]
I
InclEq [in Stalmarck.OrderedListEq]InEq [in Stalmarck.OrderedListEq]
inExpr [in Stalmarck.refl]
inRExpr [in Stalmarck.normalize]
inter [in Stalmarck.OrderedListEq]
O
Olist [in Stalmarck.OrderedListEq]OlistArray [in Stalmarck.wfArray]
Option [in Stalmarck.Option]
P
pointerDecrease [in Stalmarck.wfArray]pointToClassClass [in Stalmarck.wfArray]
pointToClassRef [in Stalmarck.wfArray]
POption [in Stalmarck.refl]
Q
Quatuor [in Stalmarck.algoDotriplets]R
rArray [in Stalmarck.rZ]rArrayP [in Stalmarck.refl]
rBoolOp [in Stalmarck.normalize]
rExpr [in Stalmarck.normalize]
rTree [in Stalmarck.rZ]
rTreeP [in Stalmarck.refl]
rZ [in Stalmarck.rZ]
S
stalmarckP [in Stalmarck.stalmarck]T
Trace [in Stalmarck.trace]Triple [in Stalmarck.memoryImplement]
triplet [in Stalmarck.triplet]
tripletResult [in Stalmarck.makeTriplet]
U
unionStateP [in Stalmarck.unionState]V
vM [in Stalmarck.wfArray]W
wellFormedArray [in Stalmarck.wfArray]Section Index
A
AaddD [in Stalmarck.addArray]algo [in Stalmarck.algoDotriplet]
algos [in Stalmarck.algoDotriplets]
Auxrem [in Stalmarck.PolyListAux]
D
Deval [in Stalmarck.memoryImplement]Dprop [in Stalmarck.memoryImplement]
I
inter [in Stalmarck.interImplement]inter [in Stalmarck.interImplement2]
L
lt [in Stalmarck.ltState]O
odilemma1 [in Stalmarck.algoDilemma1]OrderedList [in Stalmarck.OrderedListEq]
orun [in Stalmarck.algoRun]
ostal [in Stalmarck.algoStalmarck]
R
rA [in Stalmarck.rZ]rA [in Stalmarck.refl]
refl [in Stalmarck.refl]
W
wfArray [in Stalmarck.wfArray]Definition Index
A
addEq [in Stalmarck.state]addEqMem [in Stalmarck.memoryImplement]
addEqMem2 [in Stalmarck.memoryImplement]
addInterAux [in Stalmarck.interImplement2]
appendf [in Stalmarck.OrderedListEq]
appendRz [in Stalmarck.addArray]
appL [in Stalmarck.algoTrace]
appTrace [in Stalmarck.algoDotriplets]
B
boolDec [in Stalmarck.stalmarck]boolOpFun [in Stalmarck.normalize]
buildL [in Stalmarck.algoTrace]
C
checkTracef [in Stalmarck.algoTrace]CNat [in Stalmarck.OrderedListEq_ex]
contradictory [in Stalmarck.state]
CZ [in Stalmarck.OrderedListEq_ex]
D
diffElem [in Stalmarck.OrderedListEq]dilemmaN [in Stalmarck.algoDilemma1]
dilemma1 [in Stalmarck.algoDilemma1]
dilemma1R [in Stalmarck.algoDilemma1]
dilemma1RR [in Stalmarck.algoDilemma1]
dilemma1RRL [in Stalmarck.algoDilemma1]
DisjointRz [in Stalmarck.memoryImplement]
DisjointRz [in Stalmarck.wfArray]
doTripletF [in Stalmarck.algoDotriplet]
doTripletFs [in Stalmarck.algoDotriplets]
doTripletsN [in Stalmarck.algoDotriplets]
doTripletsR [in Stalmarck.algoDotriplets]
dT [in Stalmarck.algoDilemma1]
E
eqADec [in Stalmarck.OrderedListEq]eqConstrStateDec [in Stalmarck.stateDec]
eqOp [in Stalmarck.Extract]
eqRz [in Stalmarck.rZ]
eqState [in Stalmarck.state]
eqStateDec [in Stalmarck.stateDec]
eqStateRzContrDec [in Stalmarck.stateDec]
eqStateRzContrDec2 [in Stalmarck.complete]
eqStateRzDec [in Stalmarck.stateDec]
eqTriv [in Stalmarck.OrderedListEq_ex]
eqTrivZ [in Stalmarck.OrderedListEq_ex]
equalBefore [in Stalmarck.equalBefore]
Eval [in Stalmarck.normalize]
evalN [in Stalmarck.memoryImplement]
evalTraceF [in Stalmarck.algoTrace]
evalZ [in Stalmarck.memoryImplement]
ExprToProp [in Stalmarck.refl]
extendFun [in Stalmarck.equalBefore]
F
fappendf [in Stalmarck.OrderedListEq]fappendRz [in Stalmarck.addArray]
fInT [in Stalmarck.algoTrace]
fnAux [in Stalmarck.stateExtra]
FStalCorrect [in Stalmarck.algoDotriplets]
G
getB [in Stalmarck.algoRun]getClassN [in Stalmarck.memoryImplement]
getEquiv [in Stalmarck.interImplement]
getEquivList [in Stalmarck.interImplement]
getEquivMin [in Stalmarck.interImplement]
getEquivProp [in Stalmarck.interImplement]
getMin [in Stalmarck.OrderedListEq]
getMinId [in Stalmarck.interImplement]
getMinInv [in Stalmarck.interImplement]
getRzMin [in Stalmarck.interImplement]
getT [in Stalmarck.algoTrace]
I
inclState [in Stalmarck.state]inclStateDec [in Stalmarck.stateDec]
inclStateDecBis [in Stalmarck.stateDec]
InDec [in Stalmarck.algoTrace]
InEqDec [in Stalmarck.OrderedListEq]
inExprDec [in Stalmarck.refl]
InRz [in Stalmarck.memoryImplement]
InRz [in Stalmarck.wfArray]
interf [in Stalmarck.OrderedListEq]
interMem [in Stalmarck.interImplement2]
interMemProp [in Stalmarck.interImplement2]
interState [in Stalmarck.interState]
interStateP [in Stalmarck.interState]
inTriplet [in Stalmarck.triplet]
inTripletDec [in Stalmarck.triplet]
inTriplets [in Stalmarck.triplet]
inTripletsDec [in Stalmarck.triplet]
L
letP [in Stalmarck.memoryImplement]LetP [in Stalmarck.LetP]
liftRz [in Stalmarck.rZ]
listDec [in Stalmarck.wfArray]
ltState [in Stalmarck.ltState]
M
makeTriplets [in Stalmarck.makeTriplet]makeTripletsFun [in Stalmarck.makeTriplet]
max [in Stalmarck.rZ]
maxVar [in Stalmarck.normalize]
maxVarTriplet [in Stalmarck.triplet]
maxVarTriplets [in Stalmarck.triplet]
mbD [in Stalmarck.memoryImplement]
mbDOp [in Stalmarck.memoryImplement]
mbDT [in Stalmarck.algoDotriplets]
mbDTOp [in Stalmarck.algoDotriplets]
min [in Stalmarck.rZ]
myNth [in Stalmarck.complete]
N
Ncount [in Stalmarck.ltState]norm [in Stalmarck.normalize]
normImpl [in Stalmarck.normalize]
normNot [in Stalmarck.normalize]
normOr [in Stalmarck.normalize]
Nrel [in Stalmarck.ltState]
nthTail [in Stalmarck.complete]
O
olistDiff [in Stalmarck.OrderedListEq]OlistRz [in Stalmarck.memoryImplement]
OlistRz [in Stalmarck.wfArray]
oneState [in Stalmarck.ltState]
oneStateAll [in Stalmarck.ltState]
P
prodRz [in Stalmarck.interState]R
rArrayGet [in Stalmarck.rZ]rArrayGetP [in Stalmarck.refl]
rArrayInit [in Stalmarck.rZ]
rArrayInitP [in Stalmarck.refl]
rArraySet [in Stalmarck.rZ]
rArraySetList [in Stalmarck.addArray]
rArraySetP [in Stalmarck.refl]
rArrayState [in Stalmarck.memoryImplement]
rBoolOpDec [in Stalmarck.triplet]
rBoolOpFun [in Stalmarck.normalize]
realizeState [in Stalmarck.state]
realizeTriplets [in Stalmarck.triplet]
RealizeTripletsDec [in Stalmarck.complete]
rem [in Stalmarck.PolyListAux]
restrictState [in Stalmarck.restrictState]
ResTriplet [in Stalmarck.restrictState]
ResTriplets [in Stalmarck.restrictState]
rEval [in Stalmarck.normalize]
rlt [in Stalmarck.rZ]
rltDec [in Stalmarck.rZ]
rltEDec [in Stalmarck.rZ]
rmax [in Stalmarck.rZ]
rNat [in Stalmarck.rZ]
rNatDec [in Stalmarck.rZ]
rnext [in Stalmarck.rZ]
rTautology [in Stalmarck.normalize]
rTreeGet [in Stalmarck.rZ]
rTreeGetP [in Stalmarck.refl]
rTreeSet [in Stalmarck.rZ]
rTreeSetP [in Stalmarck.refl]
run [in Stalmarck.algoRun]
rVlt [in Stalmarck.rZ]
rZComp [in Stalmarck.rZ]
rZDec [in Stalmarck.rZ]
rZEval [in Stalmarck.triplet]
rZFalse [in Stalmarck.rZ]
rZlt [in Stalmarck.rZ]
rZltDec [in Stalmarck.rZ]
rZltEDec [in Stalmarck.rZ]
rZSignDec [in Stalmarck.rZ]
rZTrue [in Stalmarck.rZ]
S
samePol [in Stalmarck.rZ]samePolRz [in Stalmarck.rZ]
stal [in Stalmarck.algoStalmarck]
stalN [in Stalmarck.algoStalmarck]
State [in Stalmarck.state]
stateAssignedOn [in Stalmarck.complete]
stripInRz [in Stalmarck.restrictState]
stripRz [in Stalmarck.interState]
stripRzDec [in Stalmarck.interState]
T
Tautology [in Stalmarck.normalize]tEval [in Stalmarck.triplet]
TraceInList [in Stalmarck.trace]
tripletDec [in Stalmarck.triplet]
tTautology [in Stalmarck.makeTriplet]
U
unionState [in Stalmarck.unionState]updateArray [in Stalmarck.addArray]
updateArrayOlist [in Stalmarck.addArray]
updateArrayPointerDecrease [in Stalmarck.addArray]
V
validEquation [in Stalmarck.triplet]valRz [in Stalmarck.rZ]
valState [in Stalmarck.ltState]
varTriplets [in Stalmarck.triplet]
vMDec [in Stalmarck.wfArray]
Z
zero [in Stalmarck.rZ]| 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 | (1031 entries) |
| Variable 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) |
| 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 | (40 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 | (557 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 | (112 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 | (39 entries) |
| Section 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 | (17 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 | (174 entries) |