OAI/Analysis/Triangular/Signs/Signs00.lean
46 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_0line 10 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_0_calcline 18 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_1line 21 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_1_calcline 29 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_2line 32 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_2_calcline 40 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_3line 43 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_3_calcline 51 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_4line 54 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_4_calcline 62 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_5line 65 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_5_calcline 73 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_6line 76 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_6_calcline 84 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_7line 87 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_7_calcline 95 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_8line 98 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_8_calcline 106 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_9line 109 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_9_calcline 117 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_10line 120 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_10_calcline 128 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_11line 131 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_11_calcline 139 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_12line 142 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_12_calcline 150 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_13line 153 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_13_calcline 161 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_14line 164 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_14_calcline 172 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_15line 175 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_15_calcline 183 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_16line 186 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_16_calcline 194 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_17line 197 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_17_calcline 205 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_18line 208 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_18_calcline 216 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_19line 219 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_19_calcline 227 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_20line 230 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_20_calcline 238 - def
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0line 241 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_memline 242 - lemma
OAI.AtomicTriangular.FiniteCertificate.bs0_0_0_lowerline 268 - lemma
OAI.AtomicTriangular.FiniteCertificate.ordinary_sign_0_0_0line 273