Logiweb(TM)

Logiweb codex of check in pyk

Up Help

ref-0-id-0 check
ref-0-id-1 alpha
ref-0-id-2 beta
ref-0-id-3 gamma
ref-0-id-4 delta
ref-0-id-5 epsilon
ref-0-id-6 varepsilon
ref-0-id-7 zeta
ref-0-id-8 eta
ref-0-id-9 theta
ref-0-id-10 vartheta
ref-0-id-11 iota
ref-0-id-12 kappa
ref-0-id-13 lambda
ref-0-id-14 mu
ref-0-id-15 nu
ref-0-id-16 xi
ref-0-id-17 pi
ref-0-id-18 varpi
ref-0-id-19 rho
ref-0-id-20 varrho
ref-0-id-21 sigma
ref-0-id-22 varsigma
ref-0-id-23 tau
ref-0-id-24 upsilon
ref-0-id-25 phi
ref-0-id-26 chi
ref-0-id-27 psi
ref-0-id-28 omega
ref-0-id-29 Gamma
ref-0-id-30 Delta
ref-0-id-31 Theta
ref-0-id-32 Lambda
ref-0-id-33 Xi
ref-0-id-34 Pi
ref-0-id-35 Sigma
ref-0-id-36 Upsilon
ref-0-id-37 Phi
ref-0-id-38 Psi
ref-0-id-39 Omega
ref-0-id-40 cla
ref-0-id-41 clb
ref-0-id-42 clc
ref-0-id-43 cld
ref-0-id-44 cle
ref-0-id-45 clf
ref-0-id-46 clg
ref-0-id-47 clh
ref-0-id-48 cli
ref-0-id-49 clj
ref-0-id-50 clk
ref-0-id-51 cll
ref-0-id-52 clm
ref-0-id-53 cln
ref-0-id-54 clo
ref-0-id-55 clp
ref-0-id-56 clq
ref-0-id-57 clr
ref-0-id-58 cls
ref-0-id-59 clt
ref-0-id-60 clu
ref-0-id-61 clv
ref-0-id-62 clw
ref-0-id-63 clx
ref-0-id-64 cly
ref-0-id-65 clz
ref-0-id-66 statement
ref-0-id-67 proof
ref-0-id-68 meta
ref-0-id-69 math
ref-0-id-70 tactic
ref-0-id-71 unitac
ref-0-id-72 locate
ref-0-id-73 statement define " as " end define
ref-0-id-74 proof define " as " end define
ref-0-id-75 meta define " as " end define
ref-0-id-76 math define " as " end define
ref-0-id-77 tactic define " as " end define
ref-0-id-78 unitac define " as " end define
ref-0-id-79 locate define " as " end define
ref-0-id-80 ensure math " end math
ref-0-id-81 #a
ref-0-id-82 #b
ref-0-id-83 #c
ref-0-id-84 #d
ref-0-id-85 #e
ref-0-id-86 #f
ref-0-id-87 #g
ref-0-id-88 #h
ref-0-id-89 #i
ref-0-id-90 #j
ref-0-id-91 #k
ref-0-id-92 #l
ref-0-id-93 #m
ref-0-id-94 #n
ref-0-id-95 #o
ref-0-id-96 #p
ref-0-id-97 #q
ref-0-id-98 #r
ref-0-id-99 #s
ref-0-id-100 #t
ref-0-id-101 #u
ref-0-id-102 #v
ref-0-id-103 #w
ref-0-id-104 #x
ref-0-id-105 #y
ref-0-id-106 #z
ref-0-id-107 tacfresh ( " )
ref-0-id-108 unifresh ( " , " )
ref-0-id-109 L00
ref-0-id-110 L01
ref-0-id-111 L02
ref-0-id-112 L03
ref-0-id-113 L04
ref-0-id-114 L05
ref-0-id-115 L06
ref-0-id-116 L07
ref-0-id-117 L08
ref-0-id-118 L09
ref-0-id-119 L10
ref-0-id-120 L11
ref-0-id-121 L12
ref-0-id-122 L13
ref-0-id-123 L14
ref-0-id-124 L15
ref-0-id-125 L16
ref-0-id-126 L17
ref-0-id-127 L18
ref-0-id-128 L19
ref-0-id-129 L20
ref-0-id-130 L21
ref-0-id-131 L22
ref-0-id-132 L23
ref-0-id-133 L24
ref-0-id-134 L25
ref-0-id-135 L26
ref-0-id-136 L27
ref-0-id-137 L28
ref-0-id-138 L29
ref-0-id-139 L30
ref-0-id-140 L31
ref-0-id-141 L32
ref-0-id-142 L33
ref-0-id-143 L34
ref-0-id-144 L35
ref-0-id-145 L36
ref-0-id-146 L37
ref-0-id-147 L38
ref-0-id-148 L39
ref-0-id-149 L40
ref-0-id-150 L41
ref-0-id-151 L42
ref-0-id-152 L43
ref-0-id-153 L44
ref-0-id-154 L45
ref-0-id-155 L46
ref-0-id-156 L47
ref-0-id-157 L48
ref-0-id-158 L49
ref-0-id-159 L50
ref-0-id-160 L51
ref-0-id-161 L52
ref-0-id-162 L53
ref-0-id-163 L54
ref-0-id-164 L55
ref-0-id-165 L56
ref-0-id-166 L57
ref-0-id-167 L58
ref-0-id-168 L59
ref-0-id-169 L60
ref-0-id-170 L61
ref-0-id-171 L62
ref-0-id-172 L63
ref-0-id-173 L64
ref-0-id-174 L65
ref-0-id-175 L66
ref-0-id-176 L67
ref-0-id-177 L68
ref-0-id-178 L69
ref-0-id-179 L70
ref-0-id-180 L71
ref-0-id-181 L72
ref-0-id-182 L73
ref-0-id-183 L74
ref-0-id-184 L75
ref-0-id-185 L76
ref-0-id-186 L77
ref-0-id-187 L78
ref-0-id-188 L79
ref-0-id-189 L80
ref-0-id-190 L81
ref-0-id-191 L82
ref-0-id-192 L83
ref-0-id-193 L84
ref-0-id-194 L85
ref-0-id-195 L86
ref-0-id-196 L87
ref-0-id-197 L88
ref-0-id-198 L89
ref-0-id-199 L90
ref-0-id-200 L91
ref-0-id-201 L92
ref-0-id-202 L93
ref-0-id-203 L94
ref-0-id-204 L95
ref-0-id-205 L96
ref-0-id-206 L97
ref-0-id-207 L98
ref-0-id-208 L99
ref-0-id-209 False
ref-0-id-210 p.A1
ref-0-id-211 p.A2
ref-0-id-212 p.A3
ref-0-id-213 p.MP
ref-0-id-214 p.Prop
ref-0-id-215 p.IProp
ref-0-id-216 distinctvar ( " , " )
ref-0-id-217 metaavoid1 ( " , " , " )
ref-0-id-218 metaavoid1* ( " , " , " )
ref-0-id-219 objectavoid1 ( " , " , " , " )
ref-0-id-220 objectavoid1* ( " , " , " , " )
ref-0-id-221 metafree ( " , " , " , " )
ref-0-id-222 metafree* ( " , " , " , " )
ref-0-id-223 objectfree ( " , " , " , " )
ref-0-id-224 objectfree* ( " , " , " , " )
ref-0-id-225 remove ( " , " )
ref-0-id-226 metaavoid2* ( " , " , " )
ref-0-id-227 metasubst ( " , " , " )
ref-0-id-228 metasubst* ( " , " , " )
ref-0-id-229 metasubstc ( " , " , " )
ref-0-id-230 metasubstc1 ( " , " , " , " )
ref-0-id-231 metasubstc1* ( " , " , " , " )
ref-0-id-232 metasubstc2 ( " , " , " , " )
ref-0-id-233 metasubstc2* ( " , " , " , " )
ref-0-id-234 metasubstc3 ( " , " , " , " )
ref-0-id-235 expand-All ( " )
ref-0-id-236 expand-All1 ( " , " , " )
ref-0-id-237 make-string ( " , " )
ref-0-id-238 end diagnose
ref-0-id-239 Locate ( " , " , " )
ref-0-id-240 Locate1 ( " , " , " , " , " )
ref-0-id-241 error ( " , " )
ref-0-id-242 mismatch ( " , " , " )
ref-0-id-243 mismatch* ( " , " , " )
ref-0-id-244 eval-Init ( " , " )
ref-0-id-245 eval-Ponens ( " , " , " )
ref-0-id-246 eval-Probans ( " , " , " )
ref-0-id-247 eval-Verify ( " , " , " )
ref-0-id-248 eval-Curry ( " , " , " )
ref-0-id-249 eval-Uncurry ( " , " , " )
ref-0-id-250 eval-Deref ( " , " , " )
ref-0-id-251 eval-at ( " , " , " )
ref-0-id-252 eval-at1 ( " , " , " , " , " )
ref-0-id-253 eval-infer ( " , " , " , " )
ref-0-id-254 eval-endorse ( " , " , " , " )
ref-0-id-255 eval-ie ( " , " , " , " )
ref-0-id-256 eval-all ( " , " , " , " )
ref-0-id-257 eval-cut ( " , " , " )
ref-0-id-258 seqeval ( " , " )
ref-0-id-259 Repeat
ref-0-id-260 prepare proof indentation
ref-0-id-261 claiming ( " , " )
ref-0-id-262 proofcheck
ref-0-id-263 proofcheck1 ( " )
ref-0-id-264 proofcheck2 ( " )
ref-0-id-265 seqeval* ( " , " )
ref-0-id-266 premisecheck* ( " , " )
ref-0-id-267 checked ( " , " )
ref-0-id-268 premisecheck ( " , " )
ref-0-id-269 circularitycheck1 ( " , " , " , " )
ref-0-id-270 circularitycheck2 ( " , " , " , " )
ref-0-id-271 circularitycheck2* ( " , " , " , " )
ref-0-id-272 lemma1
ref-0-id-273 lemma2
ref-0-id-274 lemma2a
ref-0-id-275 lemma2b
ref-0-id-276 lemma2c
ref-0-id-277 lemma2d
ref-0-id-278 lemma2e
ref-0-id-279 lemma2f
ref-0-id-280 lemma3
ref-0-id-281 lemma4a
ref-0-id-282 lemma4b
ref-0-id-283 lemma4c
ref-0-id-284 lemma4d
ref-0-id-285 lemma4e
ref-0-id-286 lemma4f
ref-0-id-287 lemma4g
ref-0-id-288 int2string ( " , " )
ref-0-id-289 int2string1 ( " , " )
ref-0-id-290 val2term ( " , " )
ref-0-id-291 card2term ( " , " )
ref-0-id-292 univar ( " , " , " )
ref-0-id-293 pterm ( " , " )
ref-0-id-294 pterm1 ( " , " , " , " )
ref-0-id-295 pterm2 ( " , " , " )
ref-0-id-296 pterm2* ( " , " , " )
ref-0-id-297 inst ( " , " , " )
ref-0-id-298 inst* ( " , " , " )
ref-0-id-299 occur ( " , " , " )
ref-0-id-300 occur* ( " , " , " )
ref-0-id-301 unify ( " , " , " )
ref-0-id-302 unify* ( " , " , " )
ref-0-id-303 unify2 ( " , " , " )
ref-0-id-304 taceval ( " , " , " )
ref-0-id-305 taceval1 ( " , " , " )
ref-0-id-306 tacstate0
ref-0-id-307 unitac0
ref-0-id-308 tactic-push ( " , " , " )
ref-0-id-309 tactic-pop ( " , " )
ref-0-id-310 tactic-Init ( " )
ref-0-id-311 tactic-Ponens ( " )
ref-0-id-312 tactic-Probans ( " )
ref-0-id-313 tactic-Verify ( " )
ref-0-id-314 tactic-Curry ( " )
ref-0-id-315 tactic-Uncurry ( " )
ref-0-id-316 tactic-Deref ( " )
ref-0-id-317 tactic-at ( " )
ref-0-id-318 tactic-at1 ( " , " , " , " )
ref-0-id-319 tactic-at2 ( " , " , " , " , " )
ref-0-id-320 tactic-infer ( " )
ref-0-id-321 tactic-endorse ( " )
ref-0-id-322 tactic-ie ( " )
ref-0-id-323 tactic-all ( " )
ref-0-id-324 tactic-cut ( " )
ref-0-id-325 tactic-cut1 ( " , " , " )
ref-0-id-326 hook-arg
ref-0-id-327 hook-res
ref-0-id-328 hook-idx
ref-0-id-329 hook-uni
ref-0-id-330 hook-pre
ref-0-id-331 hook-cond
ref-0-id-332 hook-parm
ref-0-id-333 hook-unitac
ref-0-id-334 hook-rule
ref-0-id-335 hook-lemma
ref-0-id-336 hook-conclude
ref-0-id-337 unitac ( " )
ref-0-id-338 unitac1 ( " , " , " )
ref-0-id-339 unieval ( " , " , " )
ref-0-id-340 unitac-Init ( " )
ref-0-id-341 unitac-Conclude ( " )
ref-0-id-342 unitac-conclude ( " )
ref-0-id-343 unitac-conclude-std ( " )
ref-0-id-344 unitac-Ponens ( " )
ref-0-id-345 unitac-ponens ( " )
ref-0-id-346 unitac-Probans ( " )
ref-0-id-347 unitac-probans ( " )
ref-0-id-348 unitac-Verify ( " )
ref-0-id-349 unitac-verify ( " )
ref-0-id-350 unitac-Curry ( " )
ref-0-id-351 unitac-Uncurry ( " )
ref-0-id-352 unitac-Deref ( " )
ref-0-id-353 unitac-idest ( " )
ref-0-id-354 unitac-At ( " )
ref-0-id-355 unitac-at ( " )
ref-0-id-356 unitac-Infer ( " )
ref-0-id-357 unitac-infer ( " )
ref-0-id-358 unitac-Endorse ( " )
ref-0-id-359 unitac-endorse ( " )
ref-0-id-360 unitac-All ( " )
ref-0-id-361 unitac-all ( " )
ref-0-id-362 unitac-cut ( " )
ref-0-id-363 unitac-adapt ( " , " , " )
ref-0-id-364 unitac-rule ( " )
ref-0-id-365 unitac-rule-std ( " )
ref-0-id-366 unitac-theo ( " , " , " )
ref-0-id-367 unitac-rule0 ( " , " , " )
ref-0-id-368 unitac-rule-plus ( " , " , " )
ref-0-id-369 unitac-rule-stmt ( " , " , " , " )
ref-0-id-370 unitac-rule1 ( " , " , " )
ref-0-id-371 unitac-rule2 ( " , " , " )
ref-0-id-372 unitac-search ( " , " , " )
ref-0-id-373 unitac-search1 ( " , " , " , " , " )
ref-0-id-374 unitac-rule3 ( " , " )
ref-0-id-375 unitac-rule4 ( " , " )
ref-0-id-376 unitac-rule5 ( " , " , " , " )
ref-0-id-377 unitac-stack ( " , " , " )
ref-0-id-378 unitac-lemma ( " )
ref-0-id-379 unitac-lemma-std ( " )
ref-0-id-380 unitac-Rule ( " )
ref-0-id-381 seqcnt ( " , " )
ref-0-id-382 tactic-conclude-cut ( " )
ref-0-id-383 tactic-premise-line ( " )
ref-0-id-384 tactic-condition-line ( " )
ref-0-id-385 tactic-block ( " )
ref-0-id-386 System S
ref-0-id-387 S.S1
ref-0-id-388 S.S5
ref-0-id-389 S.reflexivity
ref-0-id-390 "#
ref-0-id-391 " plist ( " )
ref-0-id-392 " def ( " , " )
ref-0-id-393 " lhs ( " , " )
ref-0-id-394 " rhs ( " , " )
ref-0-id-395 " metadef ( " )
ref-0-id-396 " metavar ( " )
ref-0-id-397 " stmt-rhs ( " )
ref-0-id-398 " proof-rhs ( " )
ref-0-id-399 " tactic-rhs ( " )
ref-0-id-400 " unitac-rhs ( " )
ref-0-id-401 " locate-rhs ( " )
ref-0-id-402 " mathdef ( " )
ref-0-id-403 " valuedef ( " )
ref-0-id-404 " objectvar ( " )
ref-0-id-405 " objectlambda ( " )
ref-0-id-406 " objectquote ( " )
ref-0-id-407 " objectterm ( " )
ref-0-id-408 " objectterm* ( " )
ref-0-id-409 " metaterm ( " )
ref-0-id-410 " metaterm* ( " )
ref-0-id-411 " metaavoid ( " ) "
ref-0-id-412 " metaavoid* ( " ) "
ref-0-id-413 " objectavoid ( " ) "
ref-0-id-414 " objectavoid* ( " ) "
ref-0-id-415 " set+ "
ref-0-id-416 " set- "
ref-0-id-417 " set-- "
ref-0-id-418 " union "
ref-0-id-419 " member "
ref-0-id-420 " subset "
ref-0-id-421 " set= "
ref-0-id-422 " sequent= "
ref-0-id-423 p.not "
ref-0-id-424 " p.imply "
ref-0-id-425 metadeclare "
ref-0-id-426 " Init
ref-0-id-427 " Ponens
ref-0-id-428 " Probans
ref-0-id-429 " Verify
ref-0-id-430 " Curry
ref-0-id-431 " Uncurry
ref-0-id-432 " Deref
ref-0-id-433 " At
ref-0-id-434 " Infer
ref-0-id-435 " Endorse
ref-0-id-436 " All
ref-0-id-437 " Conclude
ref-0-id-438 " Rule
ref-0-id-439 " at "
ref-0-id-440 " ponens "
ref-0-id-441 " probans "
ref-0-id-442 " verify "
ref-0-id-443 " p.mp "
ref-0-id-444 " infer "
ref-0-id-445 " endorse "
ref-0-id-446 " id est "
ref-0-id-447 All " : "
ref-0-id-448 " oplus "
ref-0-id-449 " conclude "
ref-0-id-450 line " : " >> " ; "
ref-0-id-451 Line " : " >> " ; "
ref-0-id-452 line " : " >> " ;
ref-0-id-453 line " : " >> " qed
ref-0-id-454 line " : Premise >> " ; "
ref-0-id-455 Line " : Premise >> " ; "
ref-0-id-456 line " : Condition >> " ; "
ref-0-id-457 Line " : Condition >> " ; "
ref-0-id-458 line " : Arbitrary >> " ; "
ref-0-id-459 line " : Local >> " = " ; "
ref-0-id-460 line " : Block >> Begin ; " line " : Block >> End ; "
ref-0-id-461 Line " : Block >> Begin ; " line " : Block >> End ; "
ref-0-id-462 " ;; "
ref-0-id-463 " proves "
ref-0-id-464 axiom " : " end axiom
ref-0-id-465 rule " : " end rule
ref-0-id-466 theory " : " end theory
ref-0-id-467 lemma " : " end lemma
ref-0-id-468 " lemma " : " end lemma
ref-0-id-469 proof of " : "
ref-0-id-470 " proof of " : "
ref-0-id-471 dbug ( " ) "
ref-0-id-472 dbug* ( " ) "
ref-0-id-473 glue ( " ) "
ref-0-id-474 diag ( " ) "
ref-0-id-475 disp ( " ) "
ref-0-id-476 form ( " ) "
ref-0-id-477 glue' ( " ) "
ref-0-id-478 dbug' ( " ) "
ref-0-id-479 diag' ( " ) "
ref-0-id-480 disp' ( " ) "
ref-0-id-481 form' ( " ) "
ref-0-id-482 LocateProofLine ( " , " ) "

The pyk compiler, version 0.1.9 by Klaus Grue,
GRD-2007-07-12.UTC:20:11:58.175987 = MJD-54293.TAI:20:12:31.175987 = LGT-4690987951175987e-6