Step
*
1
of Lemma
alpha-rename-alist-property
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
⊢ (∀x,x':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (<y, y'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (x' = y' ∈ varname())
⇒ (x = y ∈ varname())))
BY
{ (Assert (L @ all-vars(t) ⊆ fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))
∧ (∀x,x':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (x' ∈ fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))))))
∧ (∀x,x':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (<y, y'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (x' = y' ∈ varname())
⇒ (x = y ∈ varname())))⋅
THENM (D -1 THEN Trivial)
) }
1
.....assertion.....
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
⊢ (L @ all-vars(t) ⊆ fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))
∧ (∀x,x':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (x' ∈ fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))))))
∧ (∀x,x':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ ((x ∈ L) ∧ (¬(x' ∈ L @ all-vars(t))))))
∧ (∀x,x',y,y':varname().
((<x, x'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (<y, y'> ∈ snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe_new_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
⇒ (x' = y' ∈ varname())
⇒ (x = y ∈ varname())))
Latex:
Latex:
1. [opr] : Type
2. t : term(opr)
3. L : varname() List
\mvdash{} (\mforall{}x,x':varname().
((<x, x'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} ((x \mmember{} L) \mwedge{} (\mneg{}(x' \mmember{} L @ all-vars(t))))))
\mwedge{} (\mforall{}x,x',y,y':varname().
((<x, x'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} (<y, y'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} (x' = y')
{}\mRightarrow{} (x = y)))
By
Latex:
(Assert (L @ all-vars(t) \msubseteq{} fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))
\mwedge{} (\mforall{}x,x':varname().
((<x, x'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} (x' \mmember{} fst(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>))))))
\mwedge{} (\mforall{}x,x':varname().
((<x, x'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} ((x \mmember{} L) \mwedge{} (\mneg{}(x' \mmember{} L @ all-vars(t))))))
\mwedge{} (\mforall{}x,x',y,y':varname().
((<x, x'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} (<y, y'> \mmember{} snd(accumulate (with value p and list item x):
let vs,tab = p
in eval x' = maybe\_new\_var(x;vs) in
<[x' / vs], [<x, x'> / tab]>
over list:
L
with starting value:
<L @ all-vars(t), []>)))
{}\mRightarrow{} (x' = y')
{}\mRightarrow{} (x = y)))\mcdot{}
THENM (D -1 THEN Trivial)
)
Home
Index