gapt-examples
gapt-examples
API
gapt.examples
church_numerals
cond
int_of_num
is_num
num
plus
times
hoare
addition
array_init
induction
associativity
associativitySpecialCase
comm
evenodd
factorial
primeFactor
nd
AndLeftWithEmptySuccedent
OrLeftWithEmptySuccedent
classicalPairing
contractRightWithWrongFocus
cut1
cut2
definitionLeftRule
definitionRightRule
definitionRightRule2
demorgan1
demorgan2
dne
equalityLeft
equalityLeftEmptySuc
equalityRight
ex0_1_6
ex0_1_6_short
example1
impLeft1
impLeft2
impRight1
impRight2
induction
inductionRule
issue687
issue688
lem
negLeft
negLeftFollowedByNegRight
negLeftRight1
negRight1
orLeft1
orLeft2
orLeft3
orLeft4
orLeft5
orRight1
orRight2
proofLink
proofLink2
proofLink3
weakenContractRight1
weakeningRight
weakeningRight1
weakeningRight2
weakeningRightWithWrongFocus
poset
cutintro
proof
predicateEliminationProblems
induction
modalCorrespondence
prime
PrimeDefinitions
euclid
euclid3
furstenberg
furstenberg3
furstenbergWitness
Multiset
ZZMPolynomial
ZZMPolynomial
recschem
vtrat_comparison
sequence
AllQuantifiedConditionalAxiomHelper
ExplicitEqualityTactics
FactorialFunctionEqualityExampleProof
FactorialFunctionEqualityExampleProof2
LinearCutExampleProof
LinearEqExampleProof
LinearExampleProof
LinearRightCutExampleProof
ProofSequence
SquareDiagonalExampleProof
SquareEdges2DimExampleProof
SquareEdgesExampleProof
SumExampleProof
SumOfOnesExampleProof
SumOfOnesF2ExampleProof
SumOfOnesFExampleProof
UniformAssociativity3ExampleProof
theories
Theory
DelayedProofResult
DelayedProofResult
Theory
LemmaHandle
LemmaHandle
Theory0
fta
list
listdrop
listfold
listlength
logic
nat
natdivisible
natdivision
natlists
natorder
props
set
tip
grammars
simp_expr_unambig1
isaplanner
prop_03
prop_06
prop_07
prop_08
prop_09
prop_10
prop_11
prop_12
prop_13
prop_14
prop_15
prop_16
prop_17
prop_18
prop_19
prop_21
prop_22
prop_23
prop_24
prop_26
prop_27
prop_28
prop_29
prop_30
prop_31
prop_32
prop_33
prop_34
prop_35
prop_36
prop_37
prop_38
prop_39
prop_40
prop_41
prop_42
prop_43
prop_44
prop_45
prop_46
prop_47
prop_48
prop_49
prop_59
prod
prop_01
prop_04
prop_05
prop_06
prop_07
prop_08
prop_10
prop_13
prop_15
prop_16
prop_20
prop_27
prop_28
prop_29
prop_30
prop_31
prop_32
prop_33
prop_34
prop_35
BussTautology
CASCData
CASCEvaluation
CERESExpansionExampleProof
CountingEquivalence
ECSJumpSchema
EventuallyConstantSchema
EventuallyConstantSchemaInductionRefutation
EventuallyConstantSchemaRefutation
ExponentialCompression
FirstSchema0
FirstSchema1
FirstSchema2
FirstSchema3
FirstSchema4
FirstSchema5
FirstSchema6
FirstSchema7
FirstSchema8
FirstSchema9
Formulas
Peano
FourStrictMonotoneSchema
FunctionIterationRefutation
FunctionIterationRefutationPos
FunctionIterationSchema
GradedStrictMonotoneSchema
GradedStrictMonotoneSequenceRefutation
GradedStrictMonotoneSequenceSchema
MonoidCancellation
NdiffSchema
NiaSchema
NiaSchemaRefutation
OneStrictMonotoneRefutation
OneStrictMonotoneSchema
OneStrictMonotoneSequenceRefutation
OneStrictMonotoneSequenceSchema
PQPairs
Permutations
Pi2Pigeonhole
Pi3Pigeonhole
PigeonHolePrinciple
ReductionDemo
ReforestDemo
Script
SimpleMutualInductionSchema
StrictMonotoneSchema
StrongStrictMonotoneSchema
ThreeStrictMonotoneRefutation
ThreeStrictMonotoneSchema
TwoStrictMonotoneRefutation
TwoStrictMonotoneSchema
VeryWeakLexicoPHPSchema
VeryWeakLexicoPHPSchemaVariant
VeryWeakLexicoPHPSchemaVariantRefutation
VeryWeakPHPSeqSchema
VeryWeakPHPSeqTwoSchema
VeryWeakPHPSequenceVariantSchema
divisionByTwo
drinker
elemAtIndex
epsilon
fol1
fol2
gapticExamples
gniaSchema
implicationLeftMacro
instprover
lattice
nTape2
nTape2
nTape3
nTape3
nTape4
nTape4
nTape5
nTape5
nTape5Arith
nTape5Arith
nTape6
formulas
sequents
nTapeInstances
philsci
primediv
successor
tape
tapeUrban
tautSchema
tbillc
gapt-examples
/
gapt.examples
/
gapt.examples.tip
gapt.examples.tip
gapt.examples.tip
package
gapt.examples.tip
Members list
Clear all
Packages
package
gapt.examples.tip.grammars
package
gapt.examples.tip.isaplanner
package
gapt.examples.tip.prod
In this article
Members list
Packages