Logiweb codex of base in pyk

Up Help

ref-0-id-0	base
ref-0-id-1	proclaim {MissingArg} as {MissingArg} end proclaim
ref-0-id-2	unicode start of text {MissingArg} end unicode text
ref-0-id-3	unicode end of text
ref-0-id-4	{MissingArg} , {MissingArg}
ref-0-id-5	{MissingArg} [ {MissingArg} ] {MissingArg}
ref-0-id-6	preassociative {MissingArg} greater than {MissingArg}
ref-0-id-7	postassociative {MissingArg} greater than {MissingArg}
ref-0-id-8	priority {MissingArg} equal {MissingArg}
ref-0-id-9	priority {MissingArg} end priority
ref-0-id-10	unicode newline {MissingArg}
ref-0-id-11	x
ref-0-id-12	text {MissingArg} end text
ref-0-id-13	text {MissingArg} plus {MissingArg}
ref-0-id-14	text {MissingArg} plus indent {MissingArg}
ref-0-id-15	pyk
ref-0-id-16	define {MissingArg} of {MissingArg} as {MissingArg} end define
ref-0-id-17	{MissingArg} linebreak {MissingArg}
ref-0-id-18	bracket {MissingArg} end bracket
ref-0-id-19	big bracket {MissingArg} end bracket
ref-0-id-20	math {MissingArg} end math
ref-0-id-21	flush left {MissingArg} end left
ref-0-id-22	var x
ref-0-id-23	var y
ref-0-id-24	var z
ref-0-id-25	tex
ref-0-id-26	tex name
ref-0-id-27	priority
ref-0-id-28	true
ref-0-id-29	if {MissingArg} then {MissingArg} else {MissingArg} end if
ref-0-id-30	introduce {MissingArg} of {MissingArg} as {MissingArg} end introduce
ref-0-id-31	value
ref-0-id-32	unicode space {MissingArg}
ref-0-id-33	unicode exclamation mark {MissingArg}
ref-0-id-34	unicode quotation mark {MissingArg}
ref-0-id-35	unicode number sign {MissingArg}
ref-0-id-36	unicode dollar sign {MissingArg}
ref-0-id-37	unicode percent {MissingArg}
ref-0-id-38	unicode ampersand {MissingArg}
ref-0-id-39	unicode apostrophe {MissingArg}
ref-0-id-40	unicode left parenthesis {MissingArg}
ref-0-id-41	unicode right parenthesis {MissingArg}
ref-0-id-42	unicode asterisk {MissingArg}
ref-0-id-43	unicode plus sign {MissingArg}
ref-0-id-44	unicode comma {MissingArg}
ref-0-id-45	unicode hyphen {MissingArg}
ref-0-id-46	unicode period {MissingArg}
ref-0-id-47	unicode slash {MissingArg}
ref-0-id-48	unicode zero {MissingArg}
ref-0-id-49	unicode one {MissingArg}
ref-0-id-50	unicode two {MissingArg}
ref-0-id-51	unicode three {MissingArg}
ref-0-id-52	unicode four {MissingArg}
ref-0-id-53	unicode five {MissingArg}
ref-0-id-54	unicode six {MissingArg}
ref-0-id-55	unicode seven {MissingArg}
ref-0-id-56	unicode eight {MissingArg}
ref-0-id-57	unicode nine {MissingArg}
ref-0-id-58	unicode colon {MissingArg}
ref-0-id-59	unicode semicolon {MissingArg}
ref-0-id-60	unicode less than {MissingArg}
ref-0-id-61	unicode equal sign {MissingArg}
ref-0-id-62	unicode greater than {MissingArg}
ref-0-id-63	unicode question mark {MissingArg}
ref-0-id-64	unicode commercial at {MissingArg}
ref-0-id-65	unicode capital a {MissingArg}
ref-0-id-66	unicode capital b {MissingArg}
ref-0-id-67	unicode capital c {MissingArg}
ref-0-id-68	unicode capital d {MissingArg}
ref-0-id-69	unicode capital e {MissingArg}
ref-0-id-70	unicode capital f {MissingArg}
ref-0-id-71	unicode capital g {MissingArg}
ref-0-id-72	unicode capital h {MissingArg}
ref-0-id-73	unicode capital i {MissingArg}
ref-0-id-74	unicode capital j {MissingArg}
ref-0-id-75	unicode capital k {MissingArg}
ref-0-id-76	unicode capital l {MissingArg}
ref-0-id-77	unicode capital m {MissingArg}
ref-0-id-78	unicode capital n {MissingArg}
ref-0-id-79	unicode capital o {MissingArg}
ref-0-id-80	unicode capital p {MissingArg}
ref-0-id-81	unicode capital q {MissingArg}
ref-0-id-82	unicode capital r {MissingArg}
ref-0-id-83	unicode capital s {MissingArg}
ref-0-id-84	unicode capital t {MissingArg}
ref-0-id-85	unicode capital u {MissingArg}
ref-0-id-86	unicode capital v {MissingArg}
ref-0-id-87	unicode capital w {MissingArg}
ref-0-id-88	unicode capital x {MissingArg}
ref-0-id-89	unicode capital y {MissingArg}
ref-0-id-90	unicode capital z {MissingArg}
ref-0-id-91	unicode left bracket {MissingArg}
ref-0-id-92	unicode backslash {MissingArg}
ref-0-id-93	unicode right bracket {MissingArg}
ref-0-id-94	unicode circumflex {MissingArg}
ref-0-id-95	unicode underscore {MissingArg}
ref-0-id-96	unicode grave accent {MissingArg}
ref-0-id-97	unicode small a {MissingArg}
ref-0-id-98	unicode small b {MissingArg}
ref-0-id-99	unicode small c {MissingArg}
ref-0-id-100	unicode small d {MissingArg}
ref-0-id-101	unicode small e {MissingArg}
ref-0-id-102	unicode small f {MissingArg}
ref-0-id-103	unicode small g {MissingArg}
ref-0-id-104	unicode small h {MissingArg}
ref-0-id-105	unicode small i {MissingArg}
ref-0-id-106	unicode small j {MissingArg}
ref-0-id-107	unicode small k {MissingArg}
ref-0-id-108	unicode small l {MissingArg}
ref-0-id-109	unicode small m {MissingArg}
ref-0-id-110	unicode small n {MissingArg}
ref-0-id-111	unicode small o {MissingArg}
ref-0-id-112	unicode small p {MissingArg}
ref-0-id-113	unicode small q {MissingArg}
ref-0-id-114	unicode small r {MissingArg}
ref-0-id-115	unicode small s {MissingArg}
ref-0-id-116	unicode small t {MissingArg}
ref-0-id-117	unicode small u {MissingArg}
ref-0-id-118	unicode small v {MissingArg}
ref-0-id-119	unicode small w {MissingArg}
ref-0-id-120	unicode small x {MissingArg}
ref-0-id-121	unicode small y {MissingArg}
ref-0-id-122	unicode small z {MissingArg}
ref-0-id-123	unicode left brace {MissingArg}
ref-0-id-124	unicode vertical line {MissingArg}
ref-0-id-125	unicode right brace {MissingArg}
ref-0-id-126	unicode tilde {MissingArg}
ref-0-id-127	claim
ref-0-id-128	bottom
ref-0-id-129	function f of {MissingArg} end function
ref-0-id-130	identity {MissingArg} end identity
ref-0-id-131	false
ref-0-id-132	untagged zero
ref-0-id-133	untagged one
ref-0-id-134	untagged two
ref-0-id-135	untagged three
ref-0-id-136	untagged four
ref-0-id-137	untagged five
ref-0-id-138	untagged six
ref-0-id-139	untagged seven
ref-0-id-140	untagged eight
ref-0-id-141	untagged nine
ref-0-id-142	zero
ref-0-id-143	one
ref-0-id-144	two
ref-0-id-145	three
ref-0-id-146	four
ref-0-id-147	five
ref-0-id-148	six
ref-0-id-149	seven
ref-0-id-150	eight
ref-0-id-151	nine
ref-0-id-152	var a
ref-0-id-153	var b
ref-0-id-154	var c
ref-0-id-155	var d
ref-0-id-156	var e
ref-0-id-157	var f
ref-0-id-158	var g
ref-0-id-159	var h
ref-0-id-160	var i
ref-0-id-161	var j
ref-0-id-162	var k
ref-0-id-163	var l
ref-0-id-164	var m
ref-0-id-165	var n
ref-0-id-166	var o
ref-0-id-167	var p
ref-0-id-168	var q
ref-0-id-169	var r
ref-0-id-170	var s
ref-0-id-171	var t
ref-0-id-172	var u
ref-0-id-173	var v
ref-0-id-174	var w
ref-0-id-175	tagged parenthesis {MissingArg} end tagged
ref-0-id-176	tagged if {MissingArg} then {MissingArg} else {MissingArg} end if
ref-0-id-177	array {MissingArg} is {MissingArg} end array
ref-0-id-178	left
ref-0-id-179	center
ref-0-id-180	right
ref-0-id-181	empty
ref-0-id-182	substitute {MissingArg} set {MissingArg} to {MissingArg} end substitute
ref-0-id-183	map tag {MissingArg} end tag
ref-0-id-184	raw map untag {MissingArg} end untag
ref-0-id-185	map untag {MissingArg} end untag
ref-0-id-186	normalizing untag {MissingArg} end untag
ref-0-id-187	apply {MissingArg} to {MissingArg} end apply
ref-0-id-188	apply one {MissingArg} to {MissingArg} end apply
ref-0-id-189	identifier {MissingArg} end identifier
ref-0-id-190	identifier one {MissingArg} plus id {MissingArg} end identifier
ref-0-id-191	array plus {MissingArg} and {MissingArg} end plus
ref-0-id-192	array remove {MissingArg} array {MissingArg} level {MissingArg} end remove
ref-0-id-193	array put {MissingArg} value {MissingArg} array {MissingArg} level {MissingArg} end put
ref-0-id-194	array add {MissingArg} value {MissingArg} index {MissingArg} value {MissingArg} level {MissingArg} end add
ref-0-id-195	bit {MissingArg} of {MissingArg} end bit
ref-0-id-196	bit one {MissingArg} of {MissingArg} end bit
ref-0-id-197	example rack
ref-0-id-198	vector hook
ref-0-id-199	bibliography hook
ref-0-id-200	dictionary hook
ref-0-id-201	body hook
ref-0-id-202	codex hook
ref-0-id-203	expansion hook
ref-0-id-204	code hook
ref-0-id-205	cache hook
ref-0-id-206	diagnose hook
ref-0-id-207	pyk aspect
ref-0-id-208	tex aspect
ref-0-id-209	texname aspect
ref-0-id-210	value aspect
ref-0-id-211	message aspect
ref-0-id-212	macro aspect
ref-0-id-213	definition aspect
ref-0-id-214	unpack aspect
ref-0-id-215	claim aspect
ref-0-id-216	priority aspect
ref-0-id-217	lambda identifier
ref-0-id-218	apply identifier
ref-0-id-219	true identifier
ref-0-id-220	if identifier
ref-0-id-221	quote identifier
ref-0-id-222	proclaim identifier
ref-0-id-223	define identifier
ref-0-id-224	introduce identifier
ref-0-id-225	hide identifier
ref-0-id-226	pre identifier
ref-0-id-227	post identifier
ref-0-id-228	eval {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-229	eval two {MissingArg} ref {MissingArg} id {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-230	eval three {MissingArg} function {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-231	eval four {MissingArg} arguments {MissingArg} stack {MissingArg} cache {MissingArg} end eval
ref-0-id-232	lookup {MissingArg} stack {MissingArg} default {MissingArg} end lookup
ref-0-id-233	abstract {MissingArg} term {MissingArg} stack {MissingArg} cache {MissingArg} end abstract
ref-0-id-234	quote {MissingArg} end quote
ref-0-id-235	expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-236	expand two {MissingArg} definition {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-237	expand list {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-238	macro
ref-0-id-239	macro state
ref-0-id-240	zip {MissingArg} with {MissingArg} end zip
ref-0-id-241	assoc one {MissingArg} address {MissingArg} index {MissingArg} end assoc
ref-0-id-242	protect {MissingArg} end protect
ref-0-id-243	self
ref-0-id-244	macro define {MissingArg} as {MissingArg} end define
ref-0-id-245	value define {MissingArg} as {MissingArg} end define
ref-0-id-246	intro define {MissingArg} as {MissingArg} end define
ref-0-id-247	pyk define {MissingArg} as {MissingArg} end define
ref-0-id-248	tex define {MissingArg} as {MissingArg} end define
ref-0-id-249	tex name define {MissingArg} as {MissingArg} end define
ref-0-id-250	priority table {MissingArg} end table
ref-0-id-251	macro define one
ref-0-id-252	macro define two {MissingArg} end define
ref-0-id-253	macro define three {MissingArg} end define
ref-0-id-254	macro define four {MissingArg} state {MissingArg} cache {MissingArg} definition {MissingArg} end define
ref-0-id-255	state expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-256	quote expand {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-257	quote expand two {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-258	quote expand three {MissingArg} term {MissingArg} stack {MissingArg} value {MissingArg} end expand
ref-0-id-259	quote expand star {MissingArg} term {MissingArg} stack {MissingArg} end expand
ref-0-id-260	parenthesis {MissingArg} end parenthesis
ref-0-id-261	big parenthesis {MissingArg} end parenthesis
ref-0-id-262	display {MissingArg} end display
ref-0-id-263	statement {MissingArg} end statement
ref-0-id-264	spying test {MissingArg} end test
ref-0-id-265	false spying test {MissingArg} end test
ref-0-id-266	aspect {MissingArg} subcodex {MissingArg} end aspect
ref-0-id-267	aspect {MissingArg} term {MissingArg} cache {MissingArg} end aspect
ref-0-id-268	tuple {MissingArg} end tuple
ref-0-id-269	tuple one {MissingArg} end tuple
ref-0-id-270	tuple two {MissingArg} end tuple
ref-0-id-271	let two {MissingArg} apply {MissingArg} end let
ref-0-id-272	let one {MissingArg} apply {MissingArg} end let
ref-0-id-273	claim define {MissingArg} as {MissingArg} end define
ref-0-id-274	checker
ref-0-id-275	check {MissingArg} cache {MissingArg} end check
ref-0-id-276	check two {MissingArg} cache {MissingArg} def {MissingArg} end check
ref-0-id-277	check three {MissingArg} cache {MissingArg} def {MissingArg} end check
ref-0-id-278	check list {MissingArg} cache {MissingArg} end check
ref-0-id-279	check list two {MissingArg} cache {MissingArg} value {MissingArg} end check
ref-0-id-280	test {MissingArg} end test
ref-0-id-281	false test {MissingArg} end test
ref-0-id-282	raw test {MissingArg} end test
ref-0-id-283	message
ref-0-id-284	message define {MissingArg} as {MissingArg} end define
ref-0-id-285	the statement aspect
ref-0-id-286	statement
ref-0-id-287	statement define {MissingArg} as {MissingArg} end define
ref-0-id-288	example axiom
ref-0-id-289	example scheme
ref-0-id-290	example rule
ref-0-id-291	absurdity
ref-0-id-292	contraexample
ref-0-id-293	example theory primed
ref-0-id-294	example lemma
ref-0-id-295	metavar {MissingArg} end metavar
ref-0-id-296	meta a
ref-0-id-297	meta b
ref-0-id-298	meta c
ref-0-id-299	meta d
ref-0-id-300	meta e
ref-0-id-301	meta f
ref-0-id-302	meta g
ref-0-id-303	meta h
ref-0-id-304	meta i
ref-0-id-305	meta j
ref-0-id-306	meta k
ref-0-id-307	meta l
ref-0-id-308	meta m
ref-0-id-309	meta n
ref-0-id-310	meta o
ref-0-id-311	meta p
ref-0-id-312	meta q
ref-0-id-313	meta r
ref-0-id-314	meta s
ref-0-id-315	meta t
ref-0-id-316	meta u
ref-0-id-317	meta v
ref-0-id-318	meta w
ref-0-id-319	meta x
ref-0-id-320	meta y
ref-0-id-321	meta z
ref-0-id-322	sub {MissingArg} set {MissingArg} to {MissingArg} end sub
ref-0-id-323	sub star {MissingArg} set {MissingArg} to {MissingArg} end sub
ref-0-id-324	the empty set
ref-0-id-325	example remainder
ref-0-id-326	make visible {MissingArg} end visible
ref-0-id-327	intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-328	intro {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-329	error {MissingArg} term {MissingArg} end error
ref-0-id-330	error two {MissingArg} term {MissingArg} end error
ref-0-id-331	proof {MissingArg} term {MissingArg} cache {MissingArg} end proof
ref-0-id-332	proof two {MissingArg} term {MissingArg} end proof
ref-0-id-333	sequent eval {MissingArg} term {MissingArg} end eval
ref-0-id-334	seqeval init {MissingArg} term {MissingArg} end eval
ref-0-id-335	seqeval modus {MissingArg} term {MissingArg} end eval
ref-0-id-336	seqeval modus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-337	seqeval verify {MissingArg} term {MissingArg} end eval
ref-0-id-338	seqeval verify one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-339	sequent eval plus {MissingArg} term {MissingArg} end eval
ref-0-id-340	seqeval plus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-341	seqeval minus {MissingArg} term {MissingArg} end eval
ref-0-id-342	seqeval minus one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-343	seqeval deref {MissingArg} term {MissingArg} end eval
ref-0-id-344	seqeval deref one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-345	seqeval deref two {MissingArg} term {MissingArg} sequent {MissingArg} def {MissingArg} end eval
ref-0-id-346	seqeval at {MissingArg} term {MissingArg} end eval
ref-0-id-347	seqeval at one {MissingArg} term {MissingArg} sequent {MissingArg} end eval
ref-0-id-348	seqeval infer {MissingArg} term {MissingArg} end eval
ref-0-id-349	seqeval infer one {MissingArg} term {MissingArg} premise {MissingArg} sequent {MissingArg} end eval
ref-0-id-350	seqeval endorse {MissingArg} term {MissingArg} end eval
ref-0-id-351	seqeval endorse one {MissingArg} term {MissingArg} side {MissingArg} sequent {MissingArg} end eval
ref-0-id-352	seqeval est {MissingArg} term {MissingArg} end eval
ref-0-id-353	seqeval est one {MissingArg} term {MissingArg} name {MissingArg} sequent {MissingArg} end eval
ref-0-id-354	seqeval est two {MissingArg} term {MissingArg} name {MissingArg} sequent {MissingArg} def {MissingArg} end eval
ref-0-id-355	seqeval all {MissingArg} term {MissingArg} end eval
ref-0-id-356	seqeval all one {MissingArg} term {MissingArg} variable {MissingArg} sequent {MissingArg} end eval
ref-0-id-357	seqeval cut {MissingArg} term {MissingArg} end eval
ref-0-id-358	seqeval cut one {MissingArg} term {MissingArg} forerunner {MissingArg} end eval
ref-0-id-359	seqeval cut two {MissingArg} term {MissingArg} forerunner {MissingArg} sequent {MissingArg} end eval
ref-0-id-360	computably true {MissingArg} end true
ref-0-id-361	claims {MissingArg} cache {MissingArg} ref {MissingArg} end claims
ref-0-id-362	claims two {MissingArg} cache {MissingArg} ref {MissingArg} end claims
ref-0-id-363	the proof aspect
ref-0-id-364	proof
ref-0-id-365	lemma {MissingArg} says {MissingArg} end lemma
ref-0-id-366	proof of {MissingArg} reads {MissingArg} end proof
ref-0-id-367	in theory {MissingArg} lemma {MissingArg} says {MissingArg} end lemma
ref-0-id-368	in theory {MissingArg} antilemma {MissingArg} says {MissingArg} end antilemma
ref-0-id-369	in theory {MissingArg} rule {MissingArg} says {MissingArg} end rule
ref-0-id-370	in theory {MissingArg} antirule {MissingArg} says {MissingArg} end antirule
ref-0-id-371	verifier
ref-0-id-372	verify one {MissingArg} end verify
ref-0-id-373	verify two {MissingArg} proofs {MissingArg} end verify
ref-0-id-374	verify three {MissingArg} ref {MissingArg} sequents {MissingArg} diagnose {MissingArg} end verify
ref-0-id-375	verify four {MissingArg} premises {MissingArg} end verify
ref-0-id-376	verify five {MissingArg} ref {MissingArg} array {MissingArg} sequents {MissingArg} end verify
ref-0-id-377	verify six {MissingArg} ref {MissingArg} list {MissingArg} sequents {MissingArg} end verify
ref-0-id-378	verify seven {MissingArg} ref {MissingArg} id {MissingArg} sequents {MissingArg} end verify
ref-0-id-379	cut {MissingArg} and {MissingArg} end cut
ref-0-id-380	head {MissingArg} end head
ref-0-id-381	tail {MissingArg} end tail
ref-0-id-382	rule one {MissingArg} theory {MissingArg} end rule
ref-0-id-383	rule {MissingArg} subcodex {MissingArg} end rule
ref-0-id-384	rule tactic
ref-0-id-385	plus {MissingArg} and {MissingArg} end plus
ref-0-id-386	theory {MissingArg} end theory
ref-0-id-387	theory two {MissingArg} cache {MissingArg} end theory
ref-0-id-388	theory three {MissingArg} name {MissingArg} end theory
ref-0-id-389	theory four {MissingArg} name {MissingArg} sum {MissingArg} end theory
ref-0-id-390	example axiom lemma primed
ref-0-id-391	example scheme lemma primed
ref-0-id-392	example rule lemma primed
ref-0-id-393	contraexample lemma primed
ref-0-id-394	example axiom lemma
ref-0-id-395	example scheme lemma
ref-0-id-396	example rule lemma
ref-0-id-397	contraexample lemma
ref-0-id-398	example theory
ref-0-id-399	ragged right
ref-0-id-400	ragged right expansion
ref-0-id-401	parameter term {MissingArg} stack {MissingArg} seed {MissingArg} end parameter
ref-0-id-402	parameter term star {MissingArg} stack {MissingArg} seed {MissingArg} end parameter
ref-0-id-403	instantiate {MissingArg} with {MissingArg} end instantiate
ref-0-id-404	instantiate star {MissingArg} with {MissingArg} end instantiate
ref-0-id-405	occur {MissingArg} in {MissingArg} substitution {MissingArg} end occur
ref-0-id-406	occur star {MissingArg} in {MissingArg} substitution {MissingArg} end occur
ref-0-id-407	unify {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-408	unify star {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-409	unify two {MissingArg} with {MissingArg} substitution {MissingArg} end unify
ref-0-id-410	ell a
ref-0-id-411	ell b
ref-0-id-412	ell c
ref-0-id-413	ell d
ref-0-id-414	ell e
ref-0-id-415	ell f
ref-0-id-416	ell g
ref-0-id-417	ell h
ref-0-id-418	ell i
ref-0-id-419	ell j
ref-0-id-420	ell k
ref-0-id-421	ell l
ref-0-id-422	ell m
ref-0-id-423	ell n
ref-0-id-424	ell o
ref-0-id-425	ell p
ref-0-id-426	ell q
ref-0-id-427	ell r
ref-0-id-428	ell s
ref-0-id-429	ell t
ref-0-id-430	ell u
ref-0-id-431	ell v
ref-0-id-432	ell w
ref-0-id-433	ell x
ref-0-id-434	ell y
ref-0-id-435	ell z
ref-0-id-436	ell big a
ref-0-id-437	ell big b
ref-0-id-438	ell big c
ref-0-id-439	ell big d
ref-0-id-440	ell big e
ref-0-id-441	ell big f
ref-0-id-442	ell big g
ref-0-id-443	ell big h
ref-0-id-444	ell big i
ref-0-id-445	ell big j
ref-0-id-446	ell big k
ref-0-id-447	ell big l
ref-0-id-448	ell big m
ref-0-id-449	ell big n
ref-0-id-450	ell big o
ref-0-id-451	ell big p
ref-0-id-452	ell big q
ref-0-id-453	ell big r
ref-0-id-454	ell big s
ref-0-id-455	ell big t
ref-0-id-456	ell big u
ref-0-id-457	ell big v
ref-0-id-458	ell big w
ref-0-id-459	ell big x
ref-0-id-460	ell big y
ref-0-id-461	ell big z
ref-0-id-462	ell dummy
ref-0-id-463	sequent reflexivity
ref-0-id-464	tactic reflexivity
ref-0-id-465	sequent commutativity
ref-0-id-466	tactic commutativity
ref-0-id-467	the tactic aspect
ref-0-id-468	tactic
ref-0-id-469	tactic define {MissingArg} as {MissingArg} end define
ref-0-id-470	proof expand {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-471	proof expand list {MissingArg} state {MissingArg} cache {MissingArg} end expand
ref-0-id-472	proof state
ref-0-id-473	conclude one {MissingArg} cache {MissingArg} end conclude
ref-0-id-474	conclude two {MissingArg} proves {MissingArg} cache {MissingArg} end conclude
ref-0-id-475	conclude three {MissingArg} proves {MissingArg} lemma {MissingArg} substitution {MissingArg} end conclude
ref-0-id-476	conclude four {MissingArg} lemma {MissingArg} end conclude
ref-0-id-477	{MissingArg} sub {MissingArg} end sub
ref-0-id-478	{MissingArg} intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-479	{MissingArg} intro {MissingArg} pyk {MissingArg} tex {MissingArg} end intro
ref-0-id-480	{MissingArg} intro {MissingArg} index {MissingArg} pyk {MissingArg} tex {MissingArg} name {MissingArg} end intro
ref-0-id-481	{MissingArg} intro {MissingArg} pyk {MissingArg} tex {MissingArg} name {MissingArg} end intro
ref-0-id-482	{MissingArg} prime
ref-0-id-483	{MissingArg} assoc {MissingArg} end assoc
ref-0-id-484	{MissingArg} set {MissingArg} to {MissingArg} end set
ref-0-id-485	{MissingArg} set multi {MissingArg} to {MissingArg} end set
ref-0-id-486	{MissingArg} bit nil
ref-0-id-487	{MissingArg} bit one
ref-0-id-488	binary
ref-0-id-489	{MissingArg} color {MissingArg} end color
ref-0-id-490	{MissingArg} color star {MissingArg} end color
ref-0-id-491	{MissingArg} raw head
ref-0-id-492	{MissingArg} raw tail
ref-0-id-493	{MissingArg} cardinal untag
ref-0-id-494	{MissingArg} head
ref-0-id-495	{MissingArg} tail
ref-0-id-496	{MissingArg} is singular
ref-0-id-497	{MissingArg} is cardinal
ref-0-id-498	{MissingArg} is data
ref-0-id-499	{MissingArg} is atomic
ref-0-id-500	{MissingArg} cardinal retract
ref-0-id-501	{MissingArg} tagged retract
ref-0-id-502	{MissingArg} boolean retract
ref-0-id-503	{MissingArg} ref
ref-0-id-504	{MissingArg} id
ref-0-id-505	{MissingArg} debug
ref-0-id-506	{MissingArg} root
ref-0-id-507	{MissingArg} zeroth
ref-0-id-508	{MissingArg} first
ref-0-id-509	{MissingArg} second
ref-0-id-510	{MissingArg} third
ref-0-id-511	{MissingArg} fourth
ref-0-id-512	{MissingArg} fifth
ref-0-id-513	{MissingArg} sixth
ref-0-id-514	{MissingArg} seventh
ref-0-id-515	{MissingArg} eighth
ref-0-id-516	{MissingArg} ninth
ref-0-id-517	{MissingArg} is error
ref-0-id-518	{MissingArg} is metavar
ref-0-id-519	{MissingArg} is metaclosed
ref-0-id-520	{MissingArg} is metaclosed star
ref-0-id-521	newline {MissingArg}
ref-0-id-522	macro newline {MissingArg}
ref-0-id-523	{MissingArg} apply {MissingArg}
ref-0-id-524	{MissingArg} tagged apply {MissingArg}
ref-0-id-525	{MissingArg} times {MissingArg}
ref-0-id-526	{MissingArg} times zero {MissingArg}
ref-0-id-527	{MissingArg} plus {MissingArg}
ref-0-id-528	{MissingArg} plus zero {MissingArg}
ref-0-id-529	{MissingArg} plus one {MissingArg}
ref-0-id-530	{MissingArg} minus {MissingArg}
ref-0-id-531	{MissingArg} minus zero {MissingArg}
ref-0-id-532	{MissingArg} minus one {MissingArg}
ref-0-id-533	{MissingArg} term plus {MissingArg} end plus
ref-0-id-534	{MissingArg} term union {MissingArg}
ref-0-id-535	{MissingArg} term minus {MissingArg} end minus
ref-0-id-536	{MissingArg} raw pair {MissingArg}
ref-0-id-537	{MissingArg} eager pair {MissingArg}
ref-0-id-538	{MissingArg} tagged pair {MissingArg}
ref-0-id-539	{MissingArg} untagged double {MissingArg}
ref-0-id-540	{MissingArg} pair {MissingArg}
ref-0-id-541	{MissingArg} double {MissingArg}
ref-0-id-542	{MissingArg} comma {MissingArg}
ref-0-id-543	{MissingArg} boolean equal {MissingArg}
ref-0-id-544	{MissingArg} data equal {MissingArg}
ref-0-id-545	{MissingArg} cardinal equal {MissingArg}
ref-0-id-546	{MissingArg} peano equal {MissingArg}
ref-0-id-547	{MissingArg} tagged equal {MissingArg}
ref-0-id-548	{MissingArg} math equal {MissingArg}
ref-0-id-549	{MissingArg} reduce to {MissingArg}
ref-0-id-550	{MissingArg} term equal {MissingArg}
ref-0-id-551	{MissingArg} term list equal {MissingArg}
ref-0-id-552	{MissingArg} term root equal {MissingArg}
ref-0-id-553	{MissingArg} term in {MissingArg}
ref-0-id-554	{MissingArg} term subset {MissingArg}
ref-0-id-555	{MissingArg} term set equal {MissingArg}
ref-0-id-556	{MissingArg} sequent equal {MissingArg}
ref-0-id-557	{MissingArg} free in {MissingArg}
ref-0-id-558	{MissingArg} free in star {MissingArg}
ref-0-id-559	{MissingArg} free for {MissingArg} in {MissingArg}
ref-0-id-560	{MissingArg} free for star {MissingArg} in {MissingArg}
ref-0-id-561	{MissingArg} claim in {MissingArg}
ref-0-id-562	{MissingArg} less {MissingArg}
ref-0-id-563	{MissingArg} less zero {MissingArg}
ref-0-id-564	{MissingArg} less one {MissingArg}
ref-0-id-565	not {MissingArg}
ref-0-id-566	{MissingArg} and {MissingArg}
ref-0-id-567	{MissingArg} macro and {MissingArg}
ref-0-id-568	{MissingArg} simple and {MissingArg}
ref-0-id-569	{MissingArg} claim and {MissingArg}
ref-0-id-570	{MissingArg} or {MissingArg}
ref-0-id-571	{MissingArg} parallel {MissingArg}
ref-0-id-572	{MissingArg} macro or {MissingArg}
ref-0-id-573	{MissingArg} macro imply {MissingArg}
ref-0-id-574	{MissingArg} guard {MissingArg}
ref-0-id-575	{MissingArg} spy {MissingArg}
ref-0-id-576	{MissingArg} tagged guard {MissingArg}
ref-0-id-577	{MissingArg} select {MissingArg} else {MissingArg} end select
ref-0-id-578	lambda {MissingArg} dot {MissingArg}
ref-0-id-579	tagged lambda {MissingArg} dot {MissingArg}
ref-0-id-580	tagging {MissingArg}
ref-0-id-581	open if {MissingArg} then {MissingArg} else {MissingArg}
ref-0-id-582	let {MissingArg} be {MissingArg} in {MissingArg}
ref-0-id-583	let {MissingArg} abbreviate {MissingArg} in {MissingArg}
ref-0-id-584	{MissingArg} init
ref-0-id-585	{MissingArg} modus
ref-0-id-586	{MissingArg} verify
ref-0-id-587	{MissingArg} curry plus
ref-0-id-588	{MissingArg} curry minus
ref-0-id-589	{MissingArg} dereference
ref-0-id-590	{MissingArg} at {MissingArg}
ref-0-id-591	{MissingArg} modus ponens {MissingArg}
ref-0-id-592	{MissingArg} modus probans {MissingArg}
ref-0-id-593	{MissingArg} conclude {MissingArg}
ref-0-id-594	{MissingArg} infer {MissingArg}
ref-0-id-595	{MissingArg} endorse {MissingArg}
ref-0-id-596	{MissingArg} id est {MissingArg}
ref-0-id-597	all {MissingArg} indeed {MissingArg}
ref-0-id-598	{MissingArg} rule plus {MissingArg}
ref-0-id-599	{MissingArg} cut {MissingArg}
ref-0-id-600	{MissingArg} proves {MissingArg}
ref-0-id-601	{MissingArg} proof of {MissingArg} reads {MissingArg}
ref-0-id-602	line {MissingArg} because {MissingArg} indeed {MissingArg} end line {MissingArg}
ref-0-id-603	because {MissingArg} indeed {MissingArg} qed
ref-0-id-604	line {MissingArg} premise {MissingArg} end line {MissingArg}
ref-0-id-605	line {MissingArg} side condition {MissingArg} end line {MissingArg}
ref-0-id-606	arbitrary {MissingArg} end line {MissingArg}
ref-0-id-607	locally define {MissingArg} as {MissingArg} end line {MissingArg}
ref-0-id-608	{MissingArg} tab {MissingArg}
ref-0-id-609	{MissingArg} row {MissingArg}