-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathProvabilityLogic.lean
More file actions
81 lines (80 loc) · 4.23 KB
/
Copy pathProvabilityLogic.lean
File metadata and controls
81 lines (80 loc) · 4.23 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
module -- shake: keep-all --deprecated_module: ignore
public import ProvabilityLogic.Formula.Basic
public import ProvabilityLogic.Formula.Countable
public import ProvabilityLogic.Formula.Letterless
public import ProvabilityLogic.Formula.Substitution
public import ProvabilityLogic.Gentzen.Basic
public import ProvabilityLogic.Gentzen.GLPoint3.Basic
public import ProvabilityLogic.Gentzen.GLPoint3.Kripke
public import ProvabilityLogic.Gentzen.Kripke
public import ProvabilityLogic.Gentzen.Maehara
public import ProvabilityLogic.Gentzen.S.Basic
public import ProvabilityLogic.Gentzen.S.Kripke
public import ProvabilityLogic.Gentzen.WithCut
public import ProvabilityLogic.Hilbert.Basic
public import ProvabilityLogic.Kripke.AlmostDefiningFormula
public import ProvabilityLogic.Kripke.Basic
public import ProvabilityLogic.Kripke.Cone
public import ProvabilityLogic.Kripke.Convergence
public import ProvabilityLogic.Kripke.DModelTree
public import ProvabilityLogic.Kripke.DefiningFormula
public import ProvabilityLogic.Kripke.Graft
public import ProvabilityLogic.Kripke.GraftOmega
public import ProvabilityLogic.Kripke.Linearity
public import ProvabilityLogic.Kripke.Overwrite
public import ProvabilityLogic.Kripke.Preservation
public import ProvabilityLogic.Kripke.PseudoTail
public import ProvabilityLogic.Kripke.Rank
public import ProvabilityLogic.Kripke.RootExtension
public import ProvabilityLogic.Kripke.RootedModel
public import ProvabilityLogic.Kripke.Simplification
public import ProvabilityLogic.Kripke.Tail
public import ProvabilityLogic.Kripke.ULift
public import ProvabilityLogic.Kripke.Unravelling
public import ProvabilityLogic.LabelledGentzen.Basic
public import ProvabilityLogic.LabelledGentzen.Completeness
public import ProvabilityLogic.LabelledGentzen.GLPoint3.Basic
public import ProvabilityLogic.LabelledGentzen.GLPoint3.Kripke
public import ProvabilityLogic.LabelledGentzen.Gentzen
public import ProvabilityLogic.LabelledGentzen.Kripke
public import ProvabilityLogic.LabelledGentzen.Loop
public import ProvabilityLogic.LabelledGentzen.Search
public import ProvabilityLogic.Logic.A.Basic
public import ProvabilityLogic.Logic.Basic
public import ProvabilityLogic.Logic.D.Basic
public import ProvabilityLogic.Logic.D.NotCIP
public import ProvabilityLogic.Logic.GL.Basic
public import ProvabilityLogic.Logic.GL.CIP
public import ProvabilityLogic.Logic.GL.Fixedpoint
public import ProvabilityLogic.Logic.GL.Letterless
public import ProvabilityLogic.Logic.GL.Theorems
public import ProvabilityLogic.Logic.GLPlusBoxBot.Basic
public import ProvabilityLogic.Logic.GLPoint2.Basic
public import ProvabilityLogic.Logic.GLPoint3.Basic
public import ProvabilityLogic.Logic.GLPoint3.Completeness
public import ProvabilityLogic.Logic.GLPoint3.Letterless
public import ProvabilityLogic.Logic.GLPoint3OplusBoxBot.Basic
public import ProvabilityLogic.Logic.S.Basic
public import ProvabilityLogic.Logic.S.Boxdot
public import ProvabilityLogic.Logic.S.CIP
public import ProvabilityLogic.Logic.SumNormal
public import ProvabilityLogic.Logic.SumQuasiNormal
public import ProvabilityLogic.ProvabilityLogic.Classification.A_D
public import ProvabilityLogic.ProvabilityLogic.Classification.D_S
public import ProvabilityLogic.ProvabilityLogic.Classification.GeneralTrace
public import ProvabilityLogic.ProvabilityLogic.Classification.LetterlessTrace
public import ProvabilityLogic.ProvabilityLogic.Classification.Result
public import ProvabilityLogic.ProvabilityLogic.D.Basic
public import ProvabilityLogic.ProvabilityLogic.GL.Basic
public import ProvabilityLogic.ProvabilityLogic.GL.Uniform
public import ProvabilityLogic.ProvabilityLogic.GLPlusBoxBot.Basic
public import ProvabilityLogic.ProvabilityLogic.GLPoint3.Basic
public import ProvabilityLogic.ProvabilityLogic.Interpret
public import ProvabilityLogic.ProvabilityLogic.ModifiedSolovaySentences
public import ProvabilityLogic.ProvabilityLogic.S.Basic
public import ProvabilityLogic.ProvabilityLogic.SolovaySentences
public import ProvabilityLogic.ToFoundation.FirstOrder.Arithmetic.Basic.Sigma1WitnessForm
public import ProvabilityLogic.ToFoundation.FirstOrder.Incompleteness.Reflection
public import ProvabilityLogic.ToFoundation.Vorspiel.List.Chain
public import ProvabilityLogic.ToFoundation.Vorspiel.Rel.CWF
public import ProvabilityLogic.ToFoundation.Vorspiel.Set.Basic