diff options
Diffstat (limited to 'test/golden/no-reflexive-set')
| -rw-r--r-- | test/golden/no-reflexive-set/encoding tasks.golden | 2 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/generating tasks.golden | 64 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/glossing.golden | 43 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/parsing.golden | 54 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/scanning.golden | 1 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/tokenizing.golden | 29 | ||||
| -rw-r--r-- | test/golden/no-reflexive-set/verification.golden | 1 |
7 files changed, 194 insertions, 0 deletions
diff --git a/test/golden/no-reflexive-set/encoding tasks.golden b/test/golden/no-reflexive-set/encoding tasks.golden new file mode 100644 index 0000000..dc79b95 --- /dev/null +++ b/test/golden/no-reflexive-set/encoding tasks.golden @@ -0,0 +1,2 @@ +fof(in_irrefl,conjecture,~elem(fA,fA)). +fof(in_irrefl1,axiom,![XIndAntecedent]:(elem(XIndAntecedent,fA)=>~elem(XIndAntecedent,XIndAntecedent))).
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/generating tasks.golden b/test/golden/no-reflexive-set/generating tasks.golden new file mode 100644 index 0000000..3ed340b --- /dev/null +++ b/test/golden/no-reflexive-set/generating tasks.golden @@ -0,0 +1,64 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "in_irrefl1" + , Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + ] + ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + , TermVar + ( B + ( NamedVar "IndAntecedent" ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "in_irrefl" + , taskConjecture = Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "A" ) + ] + ) + } +]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/glossing.golden b/test/golden/no-reflexive-set/glossing.golden new file mode 100644 index 0000000..a58b5b7 --- /dev/null +++ b/test/golden/no-reflexive-set/glossing.golden @@ -0,0 +1,43 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "in_irrefl" ) + ( Lemma [] + ( Quantified Universally + ( Scope + ( Connected Implication ( PropositionalConstant IsTop ) + ( Not + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "A" ) + ) + , TermVar + ( B + ( NamedVar "A" ) + ) + ] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( BySetInduction Nothing ( Qed JustificationEmpty ) ) +]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden new file mode 100644 index 0000000..3de5dcc --- /dev/null +++ b/test/golden/no-reflexive-set/parsing.golden @@ -0,0 +1,54 @@ +[ BlockLemma + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "in_irrefl" ) + ( Lemma [] + ( StmtQuantPhrase + ( QuantPhrase Universally NounPhrase ( [] ) + ( Noun + ( SgPl + { sg = + [ Just + ( Word "set" ) + ] + , pl = + [ Just + ( Word "sets" ) + ] + } + ) [] + ) + ( + [ NamedVar "A" ] + ) ( [] ) ( Nothing ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "A" ) :| [] + ) Negative + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "A" ) :| [] + ) + ) + ) + ) + ) + ) +, BlockProof + ( SourcePos + { sourceName = "test/examples/no-reflexive-set.tex" + , sourceLine = Pos 4 + , sourceColumn = Pos 1 + } + ) + ( BySetInduction Nothing ( Qed JustificationEmpty ) ) +]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/scanning.golden b/test/golden/no-reflexive-set/scanning.golden new file mode 100644 index 0000000..0637a08 --- /dev/null +++ b/test/golden/no-reflexive-set/scanning.golden @@ -0,0 +1 @@ +[]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/tokenizing.golden b/test/golden/no-reflexive-set/tokenizing.golden new file mode 100644 index 0000000..16835be --- /dev/null +++ b/test/golden/no-reflexive-set/tokenizing.golden @@ -0,0 +1,29 @@ +[ BeginEnv "proposition" +, Label "in_irrefl" +, Word "for" +, Word "all" +, Word "sets" +, BeginEnv "math" +, Variable "A" +, EndEnv "math" +, Word "we" +, Word "have" +, BeginEnv "math" +, Variable "A" +, Command "not" +, Command "in" +, Variable "A" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "proof" +, BracketL +, Word "proof" +, Word "by" +, Command "in" +, Word "-induction" +, BracketR +, Word "straightforward" +, Symbol "." +, EndEnv "proof" +]
\ No newline at end of file diff --git a/test/golden/no-reflexive-set/verification.golden b/test/golden/no-reflexive-set/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/no-reflexive-set/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |