Logiweb codex of check in pyk

Up Help

ref-1-id-19	var x
ref-1-id-20	var y
ref-0-id-0	check
ref-0-id-1	parameter term * stack * seed * end parameter
ref-0-id-2	parameter term star * stack * seed * end parameter
ref-0-id-3	instantiate * with * end instantiate
ref-0-id-4	instantiate star * with * end instantiate
ref-0-id-5	occur * in * end occur
ref-0-id-6	occur star * in * end occur
ref-0-id-7	circular * term * substitution * end circular
ref-0-id-8	circular star * term * substitution * end circular
ref-0-id-9	unify * with * substitution * end unify
ref-0-id-10	unify star * with * substitution * end unify
ref-0-id-11	unify two * with * substitution * end unify
ref-0-id-12	ell a
ref-0-id-13	ell b
ref-0-id-14	ell c
ref-0-id-15	ell d
ref-0-id-16	ell e
ref-0-id-17	ell f
ref-0-id-18	ell g
ref-0-id-19	ell h
ref-0-id-20	ell i
ref-0-id-21	ell j
ref-0-id-22	ell k
ref-0-id-23	ell l
ref-0-id-24	ell m
ref-0-id-25	ell n
ref-0-id-26	ell o
ref-0-id-27	ell p
ref-0-id-28	ell q
ref-0-id-29	ell r
ref-0-id-30	ell s
ref-0-id-31	ell t
ref-0-id-32	ell u
ref-0-id-33	ell v
ref-0-id-34	ell w
ref-0-id-35	ell x
ref-0-id-36	ell y
ref-0-id-37	ell z
ref-0-id-38	ell big a
ref-0-id-39	ell big b
ref-0-id-40	ell big c
ref-0-id-41	ell big d
ref-0-id-42	ell big e
ref-0-id-43	ell big f
ref-0-id-44	ell big g
ref-0-id-45	ell big h
ref-0-id-46	ell big i
ref-0-id-47	ell big j
ref-0-id-48	ell big k
ref-0-id-49	ell big l
ref-0-id-50	ell big m
ref-0-id-51	ell big n
ref-0-id-52	ell big o
ref-0-id-53	ell big p
ref-0-id-54	ell big q
ref-0-id-55	ell big r
ref-0-id-56	ell big s
ref-0-id-57	ell big t
ref-0-id-58	ell big u
ref-0-id-59	ell big v
ref-0-id-60	ell big w
ref-0-id-61	ell big x
ref-0-id-62	ell big y
ref-0-id-63	ell big z
ref-0-id-64	ell dummy
ref-0-id-65	reflexivity lemma
ref-0-id-66	reflexivity lemma one
ref-0-id-67	commutativity lemma
ref-0-id-68	the tactic aspect
ref-0-id-69	tactic
ref-0-id-70	tactic define * as * end define
ref-0-id-71	proof expand * state * cache * end expand
ref-0-id-72	proof expand list * state * cache * end expand
ref-0-id-73	proof state
ref-0-id-74	conclude one * cache * end conclude
ref-0-id-75	conclude two * proves * cache * end conclude
ref-0-id-76	conclude three * proves * lemma * substitution * end conclude
ref-0-id-77	* modus ponens *
ref-0-id-78	* modus probans *
ref-0-id-79	* conclude *
ref-0-id-80	* proof of * reads *
ref-0-id-81	line * because * indeed * cut *
ref-0-id-82	because * indeed * qed
ref-0-id-83	line * premise * cut *
ref-0-id-84	line * side condition * cut *
ref-0-id-85	arbitrary * cut *
ref-0-id-86	locally define * as * cut *