|
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 *
|
