Logiweb(TM)

Logiweb dictionary of Peano

Up Help

0 0 Peano
1 1 expand-all ( " )
2 3 expand-all1 ( " , " , " )
3 2 is-meta-term ( " , " )
4 0 unitac-hyp
5 1 unitac-lemma-hyp ( " )
6 1 unitac-rule-hyp ( " )
7 1 unitac-conclude-hyp ( " )
8 1 tactic-hyp ( " )
9 1 tactic-dummyhyp ( " )
10 2 tactic-ded ( " , " )
11 3 tactic-first-hyp ( " , " , " )
12 3 add-first-hyp* ( " , " , " )
13 3 add-first-hyp ( " , " , " )
14 4 tactic-next-hyp ( " , " , " , " )
15 3 add-next-hyp* ( " , " , " )
16 3 add-next-hyp ( " , " , " )
17 3 f.unitac-adapt ( " , " , " )
18 9 f.unitac-adapt-all ( " , " , " , " , " , " , " , " , " )
19 1 f.tacfresh ( " )
20 1 f.unitac-ponens ( " )
21 1 f.unitac-Ponens ( " )
22 1 f.unitac-at ( " )
23 1 f.unitac-At ( " )
24 4 sub ( " , " , " , " )
25 5 sub0 ( " , " , " , " , " )
26 5 sub1 ( " , " , " , " , " )
27 5 sub* ( " , " , " , " , " )
28 3 f.subst ( " , " , " )
29 3 f.subst* ( " , " , " )
30 2 inst ( " , " )
31 3 inst0 ( " , " , " )
32 3 inst1 ( " , " , " )
33 3 inst-strip ( " , " , " )
34 2 inst-zip ( " , " )
35 5 inst2 ( " , " , " , " , " )
36 5 inst2* ( " , " , " , " , " )
37 3 inst3 ( " , " , " )
38 3 inst3* ( " , " , " )
39 2 def ( " , " )
40 3 def0 ( " , " , " )
41 3 def0* ( " , " , " )
42 3 def1 ( " , " , " )
43 3 def2 ( " , " , " )
44 4 def3 ( " , " , " , " )
45 4 def3* ( " , " , " , " )
46 0 defcheck
47 2 checked-def ( " , " )
48 1 defcheck1 ( " )
49 2 defcheck2 ( " , " )
50 4 valid-def ( " , " , " , " )
51 4 valid-def* ( " , " , " , " )
52 0 Prop
53 0 FOL
54 0 PA
55 0 MP
56 0 Gen
57 0 Def
58 0 A1
59 0 A2
60 0 A3
61 0 A4
62 0 AP4
63 0 A5
64 0 tt
65 0 ff
66 0 S1
67 0 S2
68 0 S3
69 0 S4
70 0 S5
71 0 S6
72 0 S7
73 0 S8
74 0 S9
75 0 Mend1.8
76 0 A1'
77 0 A2'
78 0 Mend1.47b
79 0 Mend1.47c
80 0 Mend1.47d
81 0 Mend1.11b
82 0 Mend1.48d
83 0 Mend1.48e
84 0 Lnexthyp
85 0 Lcurry
86 0 LTruth
87 0 LElimHyp
88 0 LA4'
89 0 LAP4'
90 0 MP'
91 0 Gen1
92 0 Gen2
93 0 Gen3
94 0 Induction
95 0 hook-hyp
96 1 tactic-Prop ( " )
97 1 tactic-FOL ( " )
98 0 lemma-x
99 0 lemma-y
100 0 lemma-z
101 0 lemma-u
102 0 lemma-v
103 0 lemma-w
104 0 hyp
105 0 3.2a
106 0 3.2b
107 0 3.2c
108 0 3.2d
109 0 3.2e
110 0 3.2f
111 0 3.2g
112 0 3.2h
113 1 " First
114 1 " Second
115 1 " suc
116 1 not "
117 2 " and "
118 2 " or "
119 2 all " : "
120 1 f.allfunc "
121 2 exist " : "
122 1 f.existfunc "
123 2 " imply "
124 2 " when "
125 2 " iff "
126 2 " avoid "
127 1 " f.At
128 1 " Mp
129 2 " mp "
130 2 " f.at "
131 3 line " : Hypothesis >> " ; "
132 3 Line " : Hypothesis >> " ; "
133 2 line " : Deduction ; "
134 2 Line " : Deduction ; "

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:13:13.678589 = MJD-54293.TAI:20:13:46.678589 = LGT-4690988026678589e-6