my forest
isa progress
+38
-3
+1
-1
assets/music.tsv
+1
-1
assets/music.tsv
···
494
494
Tallis Salvator mundi OBTA p273 🟢
495
495
Tallis Sancte Deus 2ndCh p27
496
496
Tallis Verily, verily I say unto you AfC1 p208 🟢
497
-
Tallis Why fumeth in sight FaberTal p13 🟢
497
+
Tallis Why fumeth in sight FaberTal p13 🟢
498
498
Tallis With all our heart FaberTal p21 🟢
499
499
Tallis (attrib.) All people that on earth do dwell AfC1 p18
500
500
Tate Carol, with lullaby CfC1 p72
+5
-2
trees/isa/isa-0002.tree
+5
-2
trees/isa/isa-0002.tree
···
16
16
}
17
17
18
18
\transclude{isa-0005}
19
+
\transclude{isa-000Z}
20
+
\transclude{isa-0010}
19
21
\transclude{isa-000C}
20
-
\transclude{isa-0004}
21
22
\transclude{isa-0006}
22
23
\transclude{isa-000D}
24
+
\transclude{isa-0011}
25
+
\transclude{isa-0009}
23
26
\transclude{isa-0007}
24
27
\transclude{isa-0008}
25
-
\transclude{isa-0009}
26
28
\transclude{isa-000A}
29
+
\transclude{isa-0004}
27
30
\transclude{isa-000M}
28
31
\transclude{isa-000B}
29
32
+14
trees/isa/isa-000Z.tree
+14
trees/isa/isa-000Z.tree
···
1
+
\date{2025-11-28T05:41:54Z}
2
+
\taxon{Proof Method}
3
+
\title{\code{rule}}
4
+
\author{liamoc}
5
+
\p{Given a goal #{\llbracket A_1 \dots A_n \rrbracket \implies G} and a theorem \code{r}#{: \llbracket P_1 \dots P_n \rrbracket \implies G} (commonly an introduction rule),
6
+
\code{apply (rule r)} replaces the goal with subgoals:
7
+
\ul{\li{#{\llbracket A_1 \dots A_n \rrbracket \implies P_1 }}\li{ #{\dots}}\li{ #{\llbracket A_1 \dots A_n \rrbracket \implies P_n }}}
8
+
}
9
+
\scope{
10
+
\put\transclude/toc{false}
11
+
\subtree{
12
+
\taxon{Aside}
13
+
\p{Technically, the conclusion of the rule and the goal do not have to be exactly equal, but they must be \em{unifiable} – that is, there must be some substitution to schematic variables that makes the conclusion of the rule and the goal equal.}
14
+
}}
+10
trees/isa/isa-0010.tree
+10
trees/isa/isa-0010.tree
···
1
+
\date{2025-11-28T05:41:54Z}
2
+
\taxon{Proof Method}
3
+
\title{\code{frule} and \code{drule}}
4
+
\author{liamoc}
5
+
\p{Given a goal #{\llbracket X; A_1 \dots A_n \rrbracket \implies G} and a theorem \code{r}#{: \llbracket X; P_1 \dots P_n \rrbracket \implies Y},
6
+
\code{apply (frule r)} replaces the goal with subgoals:
7
+
\ul{\li{#{\llbracket X; A_1 \dots A_n \rrbracket \implies P_1 }}\li{ #{\dots}}\li{ #{\llbracket X; A_1 \dots A_n \rrbracket \implies P_n }}
8
+
\li{#{\llbracket X; Y; A_1 \dots A_n \rrbracket \implies G}}}
9
+
}
10
+
\p{The method \code{drule} is the same as \code{frule} except that it also deletes the assumption #{X} from the last subgoal.}
+8
trees/isa/isa-0011.tree
+8
trees/isa/isa-0011.tree
···
1
+
\date{2025-11-28T05:41:54Z}
2
+
\taxon{Proof Method}
3
+
\title{\code{erule}}
4
+
\author{liamoc}
5
+
\p{Given a goal #{\llbracket X; A_1 \dots A_n \rrbracket \implies G} and a theorem \code{r}#{: \llbracket X; P_1 \dots P_n \rrbracket \implies G} (typically an elimination rule where the conclusion is just a variable, easily unified with #{G}),
6
+
\code{apply (erule r)} replaces the goal with subgoals:
7
+
\ul{\li{#{\llbracket A_1 \dots A_n \rrbracket \implies P_1 }}\li{ #{\dots}}\li{ #{\llbracket A_1 \dots A_n \rrbracket \implies P_n }}}
8
+
}