Logiweb(TM)

Logiweb aspects of check in pyk

Up Help

The "pyk" aspect

Define pyk of check as "check" end define

The "claim" aspect

define claim of check as test1 &c proofcheck end define

The "macro" aspect

define macro of check as macro1 end define

The "priority" aspect

define priority of check as preassociative priority check equal priority base equal priority proclaim asterisk as asterisk end proclaim equal priority empty equal priority preassociative asterisk greater than asterisk equal priority postassociative asterisk greater than asterisk equal priority priority asterisk equal asterisk equal priority priority asterisk end priority equal priority asterisk equal priority pyk equal priority Define asterisk of asterisk as asterisk end define equal priority math asterisk end math equal priority display math asterisk end math equal priority make math asterisk end math equal priority a equal priority b equal priority c equal priority d equal priority e equal priority f equal priority g equal priority h equal priority i equal priority j equal priority k equal priority l equal priority m equal priority n equal priority o equal priority p equal priority q equal priority r equal priority s equal priority t equal priority u equal priority x equal priority y equal priority z equal priority v equal priority w equal priority A equal priority B equal priority C equal priority D equal priority E equal priority F equal priority G equal priority H equal priority I equal priority J equal priority K equal priority L equal priority M equal priority N equal priority O equal priority P equal priority Q equal priority R equal priority S equal priority T equal priority U equal priority V equal priority W equal priority X equal priority Y equal priority Z equal priority true equal priority quote asterisk end quote equal priority optimized define asterisk of asterisk as asterisk end define equal priority tex equal priority tex name equal priority priority equal priority value equal priority macro equal priority render equal priority claim equal priority message equal priority unpack equal priority execute equal priority executables equal priority exampleaspect0 equal priority exampleaspect1 equal priority exampleaspect2 equal priority name asterisk end name equal priority macro name asterisk end name equal priority hiding name asterisk end name equal priority hide asterisk end hide equal priority array ( asterisk ) asterisk end array equal priority left equal priority center equal priority right equal priority %% equal priority ( asterisk ) equal priority < asterisk | asterisk := asterisk > equal priority bottom equal priority false equal priority define asterisk of asterisk as asterisk end define equal priority ... equal priority --- equal priority Zero equal priority One equal priority Two equal priority Three equal priority Four equal priority Five equal priority Six equal priority Seven equal priority Eight equal priority Nine equal priority Ten equal priority Base equal priority Xor ( asterisk , asterisk , asterisk ) equal priority Carry ( asterisk , asterisk , asterisk ) equal priority Plus ( asterisk , asterisk , asterisk ) equal priority Borrow ( asterisk , asterisk , asterisk ) equal priority Compare ( asterisk , asterisk , asterisk ) equal priority Minus ( asterisk , asterisk , asterisk ) equal priority BoolTag equal priority IntTag equal priority PairTag equal priority ExTag equal priority MapTag equal priority equal1 ( asterisk , asterisk ) equal priority TheInt ( asterisk , asterisk ) equal priority int ( asterisk ) equal priority plus1 ( asterisk , asterisk ) equal priority plus2 ( asterisk , asterisk , asterisk , asterisk ) equal priority minus1 ( asterisk ) equal priority minus2 ( asterisk , asterisk ) equal priority times1 ( asterisk , asterisk ) equal priority times2 ( asterisk , asterisk , asterisk , asterisk ) equal priority lt1 ( asterisk , asterisk ) equal priority lt2 ( asterisk , asterisk , asterisk , asterisk ) equal priority reverse ( asterisk ) equal priority revappend ( asterisk , asterisk ) equal priority nth ( asterisk , asterisk ) equal priority exception equal priority map ( asterisk ) equal priority Catch ( asterisk ) equal priority catch ( asterisk ) equal priority object ( asterisk ) equal priority Object ( asterisk , asterisk , asterisk ) equal priority destruct ( asterisk ) equal priority 0 equal priority 1 equal priority 2 equal priority 3 equal priority 4 equal priority 5 equal priority 6 equal priority 7 equal priority 8 equal priority 9 equal priority numeral ( asterisk ) equal priority num1 ( asterisk , asterisk , asterisk ) equal priority num2 ( asterisk , asterisk , asterisk ) equal priority evenp ( asterisk ) equal priority oddp ( asterisk ) equal priority half ( asterisk ) equal priority small ( asterisk ) equal priority double ( asterisk , asterisk ) equal priority lognot ( asterisk ) equal priority logior ( asterisk , asterisk ) equal priority logxor ( asterisk , asterisk ) equal priority logand ( asterisk , asterisk ) equal priority logeqv ( asterisk , asterisk ) equal priority lognand ( asterisk , asterisk ) equal priority lognor ( asterisk , asterisk ) equal priority logandc1 ( asterisk , asterisk ) equal priority logandc2 ( asterisk , asterisk ) equal priority logorc1 ( asterisk , asterisk ) equal priority logorc2 ( asterisk , asterisk ) equal priority logtest ( asterisk , asterisk ) equal priority ash ( asterisk , asterisk ) equal priority ash+ ( asterisk , asterisk ) equal priority ash- ( asterisk , asterisk ) equal priority logbitp ( asterisk , asterisk ) equal priority logcount ( asterisk ) equal priority logcount1 ( asterisk ) equal priority integer-length ( asterisk ) equal priority vector-mask equal priority vector-empty ( asterisk ) equal priority vector-head1 ( asterisk ) equal priority vector-tail1 ( asterisk ) equal priority vector-cons ( asterisk , asterisk ) equal priority vector ( asterisk ) equal priority vector-suffix ( asterisk , asterisk ) equal priority vector-prefix ( asterisk , asterisk ) equal priority vector-subseq ( asterisk , asterisk , asterisk ) equal priority vector-length ( asterisk ) equal priority vector-index ( asterisk , asterisk ) equal priority vector-head ( asterisk ) equal priority vector-tail ( asterisk ) equal priority vector2byte* ( asterisk ) equal priority vector2byte*1 ( asterisk , asterisk ) equal priority bt2byte* ( asterisk ) equal priority bt2byte*1 ( asterisk , asterisk ) equal priority bt2vector ( asterisk ) equal priority revbyte*2vector ( asterisk , asterisk ) equal priority vector-revappend ( asterisk , asterisk ) equal priority vt2byte* ( asterisk ) equal priority vt2byte*1 ( asterisk , asterisk ) equal priority vt2vector ( asterisk ) equal priority floor1 ( asterisk , asterisk ) equal priority ceiling1 ( asterisk , asterisk ) equal priority round1 ( asterisk , asterisk ) equal priority floor ( asterisk , asterisk ) equal priority ceiling ( asterisk , asterisk ) equal priority truncate ( asterisk , asterisk ) equal priority round ( asterisk , asterisk ) equal priority reverse quotient ( asterisk ) equal priority length ( asterisk ) equal priority length1 ( asterisk , asterisk ) equal priority list-prefix ( asterisk , asterisk ) equal priority list-suffix ( asterisk , asterisk ) equal priority lookup ( asterisk , asterisk , asterisk ) equal priority zip ( asterisk , asterisk ) equal priority array1 ( asterisk , asterisk , asterisk ) equal priority array2 ( asterisk , asterisk , asterisk , asterisk ) equal priority array3 ( asterisk , asterisk ) equal priority array4 ( asterisk , asterisk ) equal priority array5 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority eval ( asterisk , asterisk , asterisk ) equal priority eval1 ( asterisk , asterisk , asterisk , asterisk ) equal priority spy ( asterisk ) equal priority trace ( asterisk ) equal priority print ( asterisk ) equal priority timer ( asterisk ) equal priority test1 equal priority test2 ( asterisk ) equal priority test3 ( asterisk , asterisk ) equal priority test3* ( asterisk , asterisk ) equal priority ttst1 ( asterisk ) equal priority ftst1 ( asterisk ) equal priority etst1 ( asterisk ) equal priority ttst asterisk end test equal priority ftst asterisk end test equal priority etst asterisk ; asterisk end test equal priority texname asterisk end texname equal priority testfunc1 ( asterisk ) equal priority testfunc2 ( asterisk , asterisk ) equal priority testfunc3 equal priority testfunc4 equal priority testfunc5 ( asterisk ) equal priority testfunc6 ( asterisk ) equal priority testfunc7 ( asterisk ) equal priority testfunc8 ( asterisk , asterisk ) equal priority macro1 equal priority macro2 ( asterisk ) equal priority macro3 ( asterisk , asterisk , asterisk ) equal priority macro3* ( asterisk , asterisk , asterisk ) equal priority macro4 ( asterisk ) equal priority macrostate0 equal priority stateexpand ( asterisk , asterisk , asterisk ) equal priority stateexpand* ( asterisk , asterisk , asterisk ) equal priority substitute ( asterisk , asterisk , asterisk ) equal priority substitute* ( asterisk , asterisk , asterisk ) equal priority expand ( asterisk , asterisk ) equal priority protect asterisk end protect equal priority Macro define asterisk as asterisk end define equal priority Macrodefine ( asterisk ) equal priority macro define asterisk as asterisk end define equal priority macrodefine ( asterisk ) equal priority self equal priority makeself ( asterisk ) equal priority root protect asterisk end protect equal priority rootprotect ( asterisk ) equal priority render define asterisk as asterisk end define equal priority tex define asterisk as asterisk end define equal priority tex name define asterisk as asterisk end define equal priority value define asterisk as asterisk end define equal priority message define asterisk as asterisk end define equal priority priority table asterisk equal priority verifier asterisk end verifier equal priority unpacker asterisk end unpacker equal priority renderer asterisk end renderer equal priority expander asterisk end expander equal priority executer asterisk end executer equal priority executables asterisk end executables equal priority ragged right equal priority make macro expanded version ragged right equal priority <<>> equal priority << asterisk >> equal priority tuple1 ( asterisk ) equal priority tuple2 ( asterisk , asterisk ) equal priority eager define asterisk as asterisk end define equal priority eager1 ( asterisk ) equal priority eager2 ( asterisk , asterisk , asterisk ) equal priority eager message define asterisk as asterisk end define equal priority macrolet1 ( asterisk ) equal priority destructure equal priority destructure define asterisk as asterisk end define equal priority let1 ( asterisk ) equal priority let2 ( asterisk , asterisk , asterisk , asterisk ) equal priority let3 ( asterisk , asterisk , asterisk , asterisk ) equal priority make-var ( asterisk ) equal priority make-let ( asterisk , asterisk , asterisk ) equal priority make-prime ( asterisk ) equal priority make-head ( asterisk ) equal priority make-tail ( asterisk ) equal priority back asterisk quote asterisk end quote equal priority make-root ( asterisk , asterisk ) equal priority make-pair ( asterisk , asterisk , asterisk ) equal priority make-true ( asterisk ) equal priority make-quote ( asterisk , asterisk ) equal priority make-make-root ( asterisk , asterisk , asterisk ) equal priority backquote0 ( asterisk ) equal priority backquote1 ( asterisk , asterisk , asterisk ) equal priority backquote2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority backquote2* ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority text asterisk : asterisk end text equal priority tex ( asterisk ) equal priority latex ( asterisk ) equal priority bibtex ( asterisk ) equal priority makeindex ( asterisk ) equal priority dvipdfm ( asterisk ) equal priority page ( asterisk , asterisk ) title asterisk bib asterisk main text asterisk appendix asterisk end page equal priority page1 ( asterisk ) equal priority tex-file ( asterisk , asterisk , asterisk ) equal priority tex-command ( asterisk , asterisk ) equal priority quit ( asterisk ) equal priority boot ( asterisk , asterisk , asterisk ) equal priority write ( asterisk ) equal priority read ( asterisk ) equal priority exec ( asterisk , asterisk ) equal priority int ( asterisk , asterisk ) equal priority extend ( asterisk ) equal priority extended ( asterisk ) equal priority Hello World equal priority Echo equal priority Echo1 ( asterisk ) equal priority Eecho equal priority Eecho1 ( asterisk ) equal priority alpha equal priority beta equal priority gamma equal priority delta equal priority epsilon equal priority varepsilon equal priority zeta equal priority eta equal priority theta equal priority vartheta equal priority iota equal priority kappa equal priority lambda equal priority mu equal priority nu equal priority xi equal priority pi equal priority varpi equal priority rho equal priority varrho equal priority sigma equal priority varsigma equal priority tau equal priority upsilon equal priority phi equal priority chi equal priority psi equal priority omega equal priority Gamma equal priority Delta equal priority Theta equal priority Lambda equal priority Xi equal priority Pi equal priority Sigma equal priority Upsilon equal priority Phi equal priority Psi equal priority Omega equal priority cla equal priority clb equal priority clc equal priority cld equal priority cle equal priority clf equal priority clg equal priority clh equal priority cli equal priority clj equal priority clk equal priority cll equal priority clm equal priority cln equal priority clo equal priority clp equal priority clq equal priority clr equal priority cls equal priority clt equal priority clu equal priority clv equal priority clw equal priority clx equal priority cly equal priority clz equal priority statement equal priority proof equal priority meta equal priority math equal priority tactic equal priority unitac equal priority locate equal priority statement define asterisk as asterisk end define equal priority proof define asterisk as asterisk end define equal priority meta define asterisk as asterisk end define equal priority math define asterisk as asterisk end define equal priority tactic define asterisk as asterisk end define equal priority unitac define asterisk as asterisk end define equal priority locate define asterisk as asterisk end define equal priority ensure math asterisk end math equal priority #a equal priority #b equal priority #c equal priority #d equal priority #e equal priority #f equal priority #g equal priority #h equal priority #i equal priority #j equal priority #k equal priority #l equal priority #m equal priority #n equal priority #o equal priority #p equal priority #q equal priority #r equal priority #s equal priority #t equal priority #u equal priority #v equal priority #w equal priority #x equal priority #y equal priority #z equal priority tacfresh ( asterisk ) equal priority unifresh ( asterisk , asterisk ) equal priority L00 equal priority L01 equal priority L02 equal priority L03 equal priority L04 equal priority L05 equal priority L06 equal priority L07 equal priority L08 equal priority L09 equal priority L10 equal priority L11 equal priority L12 equal priority L13 equal priority L14 equal priority L15 equal priority L16 equal priority L17 equal priority L18 equal priority L19 equal priority L20 equal priority L21 equal priority L22 equal priority L23 equal priority L24 equal priority L25 equal priority L26 equal priority L27 equal priority L28 equal priority L29 equal priority L30 equal priority L31 equal priority L32 equal priority L33 equal priority L34 equal priority L35 equal priority L36 equal priority L37 equal priority L38 equal priority L39 equal priority L40 equal priority L41 equal priority L42 equal priority L43 equal priority L44 equal priority L45 equal priority L46 equal priority L47 equal priority L48 equal priority L49 equal priority L50 equal priority L51 equal priority L52 equal priority L53 equal priority L54 equal priority L55 equal priority L56 equal priority L57 equal priority L58 equal priority L59 equal priority L60 equal priority L61 equal priority L62 equal priority L63 equal priority L64 equal priority L65 equal priority L66 equal priority L67 equal priority L68 equal priority L69 equal priority L70 equal priority L71 equal priority L72 equal priority L73 equal priority L74 equal priority L75 equal priority L76 equal priority L77 equal priority L78 equal priority L79 equal priority L80 equal priority L81 equal priority L82 equal priority L83 equal priority L84 equal priority L85 equal priority L86 equal priority L87 equal priority L88 equal priority L89 equal priority L90 equal priority L91 equal priority L92 equal priority L93 equal priority L94 equal priority L95 equal priority L96 equal priority L97 equal priority L98 equal priority L99 equal priority False equal priority p.A1 equal priority p.A2 equal priority p.A3 equal priority p.MP equal priority p.Prop equal priority p.IProp equal priority distinctvar ( asterisk , asterisk ) equal priority metaavoid1 ( asterisk , asterisk , asterisk ) equal priority metaavoid1* ( asterisk , asterisk , asterisk ) equal priority objectavoid1 ( asterisk , asterisk , asterisk , asterisk ) equal priority objectavoid1* ( asterisk , asterisk , asterisk , asterisk ) equal priority metafree ( asterisk , asterisk , asterisk , asterisk ) equal priority metafree* ( asterisk , asterisk , asterisk , asterisk ) equal priority objectfree ( asterisk , asterisk , asterisk , asterisk ) equal priority objectfree* ( asterisk , asterisk , asterisk , asterisk ) equal priority remove ( asterisk , asterisk ) equal priority metaavoid2* ( asterisk , asterisk , asterisk ) equal priority metasubst ( asterisk , asterisk , asterisk ) equal priority metasubst* ( asterisk , asterisk , asterisk ) equal priority metasubstc ( asterisk , asterisk , asterisk ) equal priority metasubstc1 ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc1* ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc2 ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc2* ( asterisk , asterisk , asterisk , asterisk ) equal priority metasubstc3 ( asterisk , asterisk , asterisk , asterisk ) equal priority expand-All ( asterisk ) equal priority expand-All1 ( asterisk , asterisk , asterisk ) equal priority make-string ( asterisk , asterisk ) equal priority end diagnose equal priority Locate ( asterisk , asterisk , asterisk ) equal priority Locate1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority error ( asterisk , asterisk ) equal priority mismatch ( asterisk , asterisk , asterisk ) equal priority mismatch* ( asterisk , asterisk , asterisk ) equal priority eval-Init ( asterisk , asterisk ) equal priority eval-Ponens ( asterisk , asterisk , asterisk ) equal priority eval-Probans ( asterisk , asterisk , asterisk ) equal priority eval-Verify ( asterisk , asterisk , asterisk ) equal priority eval-Curry ( asterisk , asterisk , asterisk ) equal priority eval-Uncurry ( asterisk , asterisk , asterisk ) equal priority eval-Deref ( asterisk , asterisk , asterisk ) equal priority eval-at ( asterisk , asterisk , asterisk ) equal priority eval-at1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority eval-infer ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-endorse ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-ie ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-all ( asterisk , asterisk , asterisk , asterisk ) equal priority eval-cut ( asterisk , asterisk , asterisk ) equal priority seqeval ( asterisk , asterisk ) equal priority Repeat equal priority prepare proof indentation equal priority claiming ( asterisk , asterisk ) equal priority proofcheck equal priority proofcheck1 ( asterisk ) equal priority proofcheck2 ( asterisk ) equal priority seqeval* ( asterisk , asterisk ) equal priority premisecheck* ( asterisk , asterisk ) equal priority checked ( asterisk , asterisk ) equal priority premisecheck ( asterisk , asterisk ) equal priority circularitycheck1 ( asterisk , asterisk , asterisk , asterisk ) equal priority circularitycheck2 ( asterisk , asterisk , asterisk , asterisk ) equal priority circularitycheck2* ( asterisk , asterisk , asterisk , asterisk ) equal priority lemma1 equal priority lemma2 equal priority lemma2a equal priority lemma2b equal priority lemma2c equal priority lemma2d equal priority lemma2e equal priority lemma2f equal priority lemma3 equal priority lemma4a equal priority lemma4b equal priority lemma4c equal priority lemma4d equal priority lemma4e equal priority lemma4f equal priority lemma4g equal priority int2string ( asterisk , asterisk ) equal priority int2string1 ( asterisk , asterisk ) equal priority val2term ( asterisk , asterisk ) equal priority card2term ( asterisk , asterisk ) equal priority univar ( asterisk , asterisk , asterisk ) equal priority pterm ( asterisk , asterisk ) equal priority pterm1 ( asterisk , asterisk , asterisk , asterisk ) equal priority pterm2 ( asterisk , asterisk , asterisk ) equal priority pterm2* ( asterisk , asterisk , asterisk ) equal priority inst ( asterisk , asterisk , asterisk ) equal priority inst* ( asterisk , asterisk , asterisk ) equal priority occur ( asterisk , asterisk , asterisk ) equal priority occur* ( asterisk , asterisk , asterisk ) equal priority unify ( asterisk , asterisk , asterisk ) equal priority unify* ( asterisk , asterisk , asterisk ) equal priority unify2 ( asterisk , asterisk , asterisk ) equal priority taceval ( asterisk , asterisk , asterisk ) equal priority taceval1 ( asterisk , asterisk , asterisk ) equal priority tacstate0 equal priority unitac0 equal priority tactic-push ( asterisk , asterisk , asterisk ) equal priority tactic-pop ( asterisk , asterisk ) equal priority tactic-Init ( asterisk ) equal priority tactic-Ponens ( asterisk ) equal priority tactic-Probans ( asterisk ) equal priority tactic-Verify ( asterisk ) equal priority tactic-Curry ( asterisk ) equal priority tactic-Uncurry ( asterisk ) equal priority tactic-Deref ( asterisk ) equal priority tactic-at ( asterisk ) equal priority tactic-at1 ( asterisk , asterisk , asterisk , asterisk ) equal priority tactic-at2 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority tactic-infer ( asterisk ) equal priority tactic-endorse ( asterisk ) equal priority tactic-ie ( asterisk ) equal priority tactic-all ( asterisk ) equal priority tactic-cut ( asterisk ) equal priority tactic-cut1 ( asterisk , asterisk , asterisk ) equal priority hook-arg equal priority hook-res equal priority hook-idx equal priority hook-uni equal priority hook-pre equal priority hook-cond equal priority hook-parm equal priority hook-unitac equal priority hook-rule equal priority hook-lemma equal priority hook-conclude equal priority unitac ( asterisk ) equal priority unitac1 ( asterisk , asterisk , asterisk ) equal priority unieval ( asterisk , asterisk , asterisk ) equal priority unitac-Init ( asterisk ) equal priority unitac-Conclude ( asterisk ) equal priority unitac-conclude ( asterisk ) equal priority unitac-conclude-std ( asterisk ) equal priority unitac-Ponens ( asterisk ) equal priority unitac-ponens ( asterisk ) equal priority unitac-Probans ( asterisk ) equal priority unitac-probans ( asterisk ) equal priority unitac-Verify ( asterisk ) equal priority unitac-verify ( asterisk ) equal priority unitac-Curry ( asterisk ) equal priority unitac-Uncurry ( asterisk ) equal priority unitac-Deref ( asterisk ) equal priority unitac-idest ( asterisk ) equal priority unitac-At ( asterisk ) equal priority unitac-at ( asterisk ) equal priority unitac-Infer ( asterisk ) equal priority unitac-infer ( asterisk ) equal priority unitac-Endorse ( asterisk ) equal priority unitac-endorse ( asterisk ) equal priority unitac-All ( asterisk ) equal priority unitac-all ( asterisk ) equal priority unitac-cut ( asterisk ) equal priority unitac-adapt ( asterisk , asterisk , asterisk ) equal priority unitac-rule ( asterisk ) equal priority unitac-rule-std ( asterisk ) equal priority unitac-theo ( asterisk , asterisk , asterisk ) equal priority unitac-rule0 ( asterisk , asterisk , asterisk ) equal priority unitac-rule-plus ( asterisk , asterisk , asterisk ) equal priority unitac-rule-stmt ( asterisk , asterisk , asterisk , asterisk ) equal priority unitac-rule1 ( asterisk , asterisk , asterisk ) equal priority unitac-rule2 ( asterisk , asterisk , asterisk ) equal priority unitac-search ( asterisk , asterisk , asterisk ) equal priority unitac-search1 ( asterisk , asterisk , asterisk , asterisk , asterisk ) equal priority unitac-rule3 ( asterisk , asterisk ) equal priority unitac-rule4 ( asterisk , asterisk ) equal priority unitac-rule5 ( asterisk , asterisk , asterisk , asterisk ) equal priority unitac-stack ( asterisk , asterisk , asterisk ) equal priority unitac-lemma ( asterisk ) equal priority unitac-lemma-std ( asterisk ) equal priority unitac-Rule ( asterisk ) equal priority seqcnt ( asterisk , asterisk ) equal priority tactic-conclude-cut ( asterisk ) equal priority tactic-premise-line ( asterisk ) equal priority tactic-condition-line ( asterisk ) equal priority tactic-block ( asterisk ) equal priority System S equal priority S.S1 equal priority S.S5 equal priority S.reflexivity end priority greater than preassociative priority +asterisk equal priority -asterisk equal priority 0asterisk equal priority 1asterisk equal priority 2asterisk equal priority 3asterisk equal priority 4asterisk equal priority 5asterisk equal priority 6asterisk equal priority 7asterisk equal priority 8asterisk equal priority 9asterisk end priority greater than preassociative priority asterisk factorial equal priority asterisk _ { asterisk } equal priority asterisk prime equal priority asterisk %0 equal priority asterisk %1 equal priority asterisk %2 equal priority asterisk %3 equal priority asterisk %4 equal priority asterisk %5 equal priority asterisk %6 equal priority asterisk %7 equal priority asterisk %8 equal priority asterisk %9 equal priority asterisk head equal priority asterisk tail equal priority asterisk raise equal priority asterisk catch equal priority asterisk catching maptag equal priority asterisk maptag equal priority asterisk untag equal priority asterisk boolp equal priority asterisk truep equal priority asterisk falsep equal priority asterisk intp equal priority asterisk pairp equal priority asterisk atom equal priority asterisk mapp equal priority asterisk objectp equal priority asterisk root equal priority asterisk Head equal priority asterisk Tail equal priority asterisk TheBool equal priority asterisk TheNat equal priority asterisk norm equal priority asterisk Tag equal priority asterisk BoolP equal priority asterisk IntP equal priority asterisk PairP equal priority asterisk ExP equal priority asterisk MapP equal priority asterisk ObjectP equal priority asterisk Sign equal priority asterisk Mag equal priority asterisk zeroth equal priority asterisk first equal priority asterisk second equal priority asterisk third equal priority asterisk fourth equal priority asterisk fifth equal priority asterisk sixth equal priority asterisk seventh equal priority asterisk eighth equal priority asterisk ninth equal priority asterisk ref equal priority asterisk idx equal priority asterisk debug equal priority asterisk [[ asterisk ]] equal priority asterisk [[ asterisk -> asterisk ]] equal priority asterisk [[ asterisk => asterisk ]] equal priority asterisk unquote equal priority asterisk# equal priority asterisk plist ( asterisk ) equal priority asterisk def ( asterisk , asterisk ) equal priority asterisk lhs ( asterisk , asterisk ) equal priority asterisk rhs ( asterisk , asterisk ) equal priority asterisk metadef ( asterisk ) equal priority asterisk metavar ( asterisk ) equal priority asterisk stmt-rhs ( asterisk ) equal priority asterisk proof-rhs ( asterisk ) equal priority asterisk tactic-rhs ( asterisk ) equal priority asterisk unitac-rhs ( asterisk ) equal priority asterisk locate-rhs ( asterisk ) equal priority asterisk mathdef ( asterisk ) equal priority asterisk valuedef ( asterisk ) equal priority asterisk objectvar ( asterisk ) equal priority asterisk objectlambda ( asterisk ) equal priority asterisk objectquote ( asterisk ) equal priority asterisk objectterm ( asterisk ) equal priority asterisk objectterm* ( asterisk ) equal priority asterisk metaterm ( asterisk ) equal priority asterisk metaterm* ( asterisk ) equal priority asterisk metaavoid ( asterisk ) asterisk equal priority asterisk metaavoid* ( asterisk ) asterisk equal priority asterisk objectavoid ( asterisk ) asterisk equal priority asterisk objectavoid* ( asterisk ) asterisk end priority greater than preassociative priority asterisk ' asterisk equal priority asterisk apply asterisk end priority greater than preassociative priority - asterisk equal priority + asterisk end priority greater than preassociative priority asterisk Times asterisk equal priority asterisk * asterisk end priority greater than preassociative priority asterisk Plus asterisk equal priority asterisk Minus asterisk equal priority asterisk + asterisk equal priority asterisk - asterisk equal priority asterisk set+ asterisk equal priority asterisk set- asterisk equal priority asterisk set-- asterisk equal priority asterisk union asterisk end priority greater than preassociative priority PlusTag asterisk equal priority MinusTag asterisk end priority greater than preassociative priority asterisk div asterisk equal priority asterisk mod asterisk end priority greater than postassociative priority asterisk LazyPair asterisk equal priority asterisk Pair asterisk equal priority asterisk NatPair asterisk equal priority asterisk :: asterisk end priority greater than postassociative priority asterisk ,, asterisk end priority greater than preassociative priority asterisk = asterisk equal priority asterisk != asterisk equal priority asterisk Equal asterisk equal priority asterisk LT asterisk equal priority asterisk < asterisk equal priority asterisk <= asterisk equal priority asterisk > asterisk equal priority asterisk >= asterisk equal priority asterisk r= asterisk equal priority asterisk t= asterisk equal priority asterisk t=* asterisk equal priority asterisk member asterisk equal priority asterisk subset asterisk equal priority asterisk set= asterisk equal priority asterisk sequent= asterisk end priority greater than preassociative priority Not asterisk equal priority .not. asterisk equal priority notnot asterisk equal priority p.not asterisk end priority greater than preassociative priority asterisk And asterisk equal priority asterisk .and. asterisk equal priority asterisk .then. asterisk equal priority asterisk &c asterisk end priority greater than preassociative priority asterisk Or asterisk equal priority asterisk .or. asterisk end priority greater than postassociative priority asterisk Iff asterisk equal priority asterisk p.imply asterisk end priority greater than preassociative priority asterisk Select asterisk else asterisk end select equal priority asterisk IN asterisk end priority greater than preassociative priority \ asterisk . asterisk equal priority If asterisk then asterisk else asterisk equal priority if asterisk then asterisk else asterisk equal priority newline asterisk equal priority LET asterisk BE asterisk equal priority let asterisk := asterisk in asterisk equal priority let asterisk = asterisk in asterisk equal priority metadeclare asterisk end priority greater than postassociative priority norm asterisk equal priority asterisk Guard asterisk equal priority asterisk is val : asterisk equal priority asterisk is bool : asterisk equal priority asterisk is int : asterisk equal priority asterisk is pair : asterisk equal priority asterisk is map : asterisk equal priority asterisk is object : asterisk end priority greater than preassociative priority asterisk reduce to asterisk equal priority asterisk == asterisk end priority greater than preassociative priority asterisk Init equal priority asterisk Ponens equal priority asterisk Probans equal priority asterisk Verify equal priority asterisk Curry equal priority asterisk Uncurry equal priority asterisk Deref equal priority asterisk At equal priority asterisk Infer equal priority asterisk Endorse equal priority asterisk All equal priority asterisk Conclude equal priority asterisk Rule end priority greater than preassociative priority asterisk at asterisk equal priority asterisk ponens asterisk equal priority asterisk probans asterisk equal priority asterisk verify asterisk equal priority asterisk p.mp asterisk end priority greater than postassociative priority asterisk infer asterisk equal priority asterisk endorse asterisk equal priority asterisk id est asterisk end priority greater than preassociative priority All asterisk : asterisk end priority greater than postassociative priority asterisk oplus asterisk end priority greater than preassociative priority asterisk conclude asterisk end priority greater than postassociative priority line asterisk : asterisk >> asterisk ; asterisk equal priority Line asterisk : asterisk >> asterisk ; asterisk equal priority line asterisk : asterisk >> asterisk ; equal priority line asterisk : asterisk >> asterisk qed equal priority line asterisk : Premise >> asterisk ; asterisk equal priority Line asterisk : Premise >> asterisk ; asterisk equal priority line asterisk : Condition >> asterisk ; asterisk equal priority Line asterisk : Condition >> asterisk ; asterisk equal priority line asterisk : Arbitrary >> asterisk ; asterisk equal priority line asterisk : Local >> asterisk = asterisk ; asterisk equal priority line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk equal priority Line asterisk : Block >> Begin ; asterisk line asterisk : Block >> End ; asterisk end priority greater than postassociative priority asterisk ;; asterisk end priority greater than preassociative priority asterisk proves asterisk end priority greater than postassociative priority axiom asterisk : asterisk end axiom equal priority rule asterisk : asterisk end rule equal priority theory asterisk : asterisk end theory equal priority lemma asterisk : asterisk end lemma equal priority asterisk lemma asterisk : asterisk end lemma equal priority proof of asterisk : asterisk equal priority asterisk proof of asterisk : asterisk end priority greater than postassociative priority asterisk,asterisk equal priority asterisk[ asterisk ]asterisk equal priority asterisk[[ asterisk ]]asterisk equal priority asterisk[[[ asterisk ]]]asterisk equal priority dbug ( asterisk ) asterisk equal priority dbug* ( asterisk ) asterisk equal priority glue ( asterisk ) asterisk equal priority diag ( asterisk ) asterisk equal priority disp ( asterisk ) asterisk equal priority form ( asterisk ) asterisk equal priority glue' ( asterisk ) asterisk equal priority dbug' ( asterisk ) asterisk equal priority diag' ( asterisk ) asterisk equal priority disp' ( asterisk ) asterisk equal priority form' ( asterisk ) asterisk equal priority LocateProofLine ( asterisk , asterisk ) asterisk end priority greater than preassociative priority asterisk linebreak asterisk end priority greater than preassociative priority asterisk & asterisk end priority greater than preassociative priority asterisk \\ asterisk end priority greater than empty end define

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