8 atom_decl name |
8 atom_decl name |
9 atom_decl coname |
9 atom_decl coname |
10 |
10 |
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Ax "name" "coname" |
12 Ax "name" "coname" |
13 | Cut c::"coname" t1::"trm" n::"name" t2::"trm" bind n in t1, bind c in t2 |
13 | Cut c::"coname" t1::"trm" n::"name" t2::"trm" binds n in t1, binds c in t2 |
14 ("Cut <_>._ '(_')._" [100,100,100,100] 100) |
14 ("Cut <_>._ '(_')._" [100,100,100,100] 100) |
15 | NotR n::"name" t::"trm" "coname" bind n in t |
15 | NotR n::"name" t::"trm" "coname" binds n in t |
16 ("NotR '(_')._ _" [100,100,100] 100) |
16 ("NotR '(_')._ _" [100,100,100] 100) |
17 | NotL c::"coname" t::"trm" "name" bind c in t |
17 | NotL c::"coname" t::"trm" "name" binds c in t |
18 ("NotL <_>._ _" [100,100,100] 100) |
18 ("NotL <_>._ _" [100,100,100] 100) |
19 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" bind c1 in t1, bind c2 in t2 |
19 | AndR c1::"coname" t1::"trm" c2::"coname" t2::"trm" "coname" binds c1 in t1, binds c2 in t2 |
20 ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100) |
20 ("AndR <_>._ <_>._ _" [100,100,100,100,100] 100) |
21 | AndL1 n::"name" t::"trm" "name" bind n in t |
21 | AndL1 n::"name" t::"trm" "name" binds n in t |
22 ("AndL1 '(_')._ _" [100,100,100] 100) |
22 ("AndL1 '(_')._ _" [100,100,100] 100) |
23 | AndL2 n::"name" t::"trm" "name" bind n in t |
23 | AndL2 n::"name" t::"trm" "name" binds n in t |
24 ("AndL2 '(_')._ _" [100,100,100] 100) |
24 ("AndL2 '(_')._ _" [100,100,100] 100) |
25 | OrR1 c::"coname" t::"trm" "coname" bind c in t |
25 | OrR1 c::"coname" t::"trm" "coname" binds c in t |
26 ("OrR1 <_>._ _" [100,100,100] 100) |
26 ("OrR1 <_>._ _" [100,100,100] 100) |
27 | OrR2 c::"coname" t::"trm" "coname" bind c in t |
27 | OrR2 c::"coname" t::"trm" "coname" binds c in t |
28 ("OrR2 <_>._ _" [100,100,100] 100) |
28 ("OrR2 <_>._ _" [100,100,100] 100) |
29 | OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" bind n1 in t1, bind n2 in t2 |
29 | OrL n1::"name" t1::"trm" n2::"name" t2::"trm" "name" binds n1 in t1, binds n2 in t2 |
30 ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100) |
30 ("OrL '(_')._ '(_')._ _" [100,100,100,100,100] 100) |
31 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" bind c in t1, bind n in t2 |
31 | ImpL c::"coname" t1::"trm" n::"name" t2::"trm" "name" binds c in t1, binds n in t2 |
32 ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100) |
32 ("ImpL <_>._ '(_')._ _" [100,100,100,100,100] 100) |
33 | ImpR n::"name" c::"coname" t::"trm" "coname" bind n c in t |
33 | ImpR n::"name" c::"coname" t::"trm" "coname" binds n c in t |
34 ("ImpR '(_').<_>._ _" [100,100,100,100] 100) |
34 ("ImpR '(_').<_>._ _" [100,100,100,100] 100) |
35 |
35 |
36 thm trm.distinct |
36 thm trm.distinct |
37 thm trm.induct |
37 thm trm.induct |
38 thm trm.exhaust |
38 thm trm.exhaust |