-
Notifications
You must be signed in to change notification settings - Fork 15
Expand file tree
/
Copy pathexisting_proofs.yml
More file actions
100 lines (100 loc) · 6.2 KB
/
existing_proofs.yml
File metadata and controls
100 lines (100 loc) · 6.2 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
1: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, NuPRL (constructive), PVS, ProofPower, Rocq (constructive)]
2: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
3: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower, Rocq (constructive)]
4: [HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq]
5: [HOL Light, Isabelle, Lean, Metamath]
6: [HOL Light, Isabelle, Lean, Rocq (constructive), nqthm]
7: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq, nqthm]
8: [HOL Light, Isabelle]
9: [ACL2, HOL Light, Isabelle, Lean, Metamath, ProofPower]
10: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq (constructive)]
11: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, PVS, ProofPower, Rocq (constructive)]
12: [HOL Light, Isabelle]
13: [HOL Light, Isabelle, Mizar, Rocq (constructive)]
14: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
15: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
16: [Lean, Rocq]
17: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
18: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq (constructive)]
19: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, Rocq (constructive)]
20: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
21: [Isabelle]
22: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
23: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq (constructive)]
24: [Isabelle, Lean]
25: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, ProofPower, Rocq]
26: [HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, Rocq (constructive)]
27: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
28: [HOL Light, Mizar, Rocq]
29: [HOL Light, Rocq (constructive)]
30: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
31: [HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower, Rocq (constructive), nqthm]
32: [Rocq]
33: []
34: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
35: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
36: [HOL Light, Isabelle, Lean, Mizar]
37: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
38: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
39: [HOL Light, Isabelle, Lean, Metamath, Mizar]
40: [HOL Light, Isabelle, Lean, ProofPower]
41: [Isabelle, Rocq]
42: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq (constructive)]
43: [HOL Light]
44: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), ProofPower, Rocq (constructive)]
45: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar]
46: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
47: [Isabelle]
48: [HOL Light, Isabelle, Lean, Metamath]
49: [HOL Light, Isabelle, Lean, Metamath, Rocq]
50: [HOL Light]
51: [HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq (constructive), nqthm]
52: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, ProofPower, Rocq (constructive)]
53: [HOL Light, Isabelle, Rocq]
54: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
55: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
56: [HOL Light, Isabelle, Rocq]
57: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq (constructive)]
58: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
59: [Isabelle, Lean, Rocq]
60: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, NuPRL (constructive), ProofPower, Rocq (constructive)]
61: [HOL Light, Isabelle, Metamath, Mizar, Rocq]
62: [Lean, Rocq]
63: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, NuPRL (constructive), ProofPower, Rocq]
64: [HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
65: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
66: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, PVS, ProofPower, Rocq (constructive)]
67: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
68: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, PVS, ProofPower, Rocq (constructive)]
69: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, NuPRL (constructive), PVS, ProofPower, Rocq (constructive)]
70: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq (constructive)]
71: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
72: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, Rocq (constructive)]
73: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
74: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Naproche, ProofPower, Rocq (constructive)]
75: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
76: [HOL Light, Isabelle, Lean, Metamath]
77: [HOL Light, Isabelle, Lean, Metamath, Rocq]
78: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq]
79: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq (constructive)]
80: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, NuPRL (constructive), PVS, ProofPower, Rocq (constructive)]
81: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower]
82: [Isabelle, Lean]
83: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq (constructive)]
84: [HOL Light, Isabelle, Mizar, Rocq]
85: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq]
86: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
87: [HOL Light, Isabelle, Metamath, Mizar, Rocq]
88: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
89: [HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq (constructive)]
90: [HOL Light, Isabelle, Lean, Metamath, Rocq]
91: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq]
92: [HOL Light, Isabelle]
93: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, ProofPower, Rocq]
94: [HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, Rocq]
95: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
96: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, PVS, ProofPower, Rocq]
97: [ACL2, HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
98: [HOL Light, Isabelle, Lean, Metamath, Mizar, Rocq]
99: [Isabelle, Lean, ProofPower]
100: [HOL Light, Isabelle, Lean, ProofPower]