86 lines
2.2 KiB
Text
86 lines
2.2 KiB
Text
|
::: ## Lambda calculus
|
||
|
|
|
||
|
|
environ
|
||
|
|
|
||
|
|
vocabularies LAMBDA,
|
||
|
|
NUMBERS,
|
||
|
|
NAT_1, XBOOLE_0, SUBSET_1, FINSEQ_1, XXREAL_0, CARD_1,
|
||
|
|
ARYTM_1, ARYTM_3, TARSKI, RELAT_1, ORDINAL4, FUNCOP_1;
|
||
|
|
|
||
|
|
:: etc...
|
||
|
|
|
||
|
|
begin
|
||
|
|
|
||
|
|
reserve D for DecoratedTree,
|
||
|
|
p,q,r for FinSequence of NAT,
|
||
|
|
x for set;
|
||
|
|
|
||
|
|
definition
|
||
|
|
let D;
|
||
|
|
|
||
|
|
attr D is LambdaTerm-like means
|
||
|
|
(dom D qua Tree) is finite &
|
||
|
|
::> *143,306
|
||
|
|
for r st r in dom D holds
|
||
|
|
r is FinSequence of {0,1} &
|
||
|
|
r^<*0*> in dom D implies D.r = 0;
|
||
|
|
end;
|
||
|
|
|
||
|
|
registration
|
||
|
|
cluster LambdaTerm-like for DecoratedTree of NAT;
|
||
|
|
existence;
|
||
|
|
::> *4
|
||
|
|
end;
|
||
|
|
|
||
|
|
definition
|
||
|
|
mode LambdaTerm is LambdaTerm-like DecoratedTree of NAT;
|
||
|
|
end;
|
||
|
|
|
||
|
|
::: Then we extend this ordinary one-step beta reduction, that is,
|
||
|
|
::: any subterm is also allowed to reduce.
|
||
|
|
definition
|
||
|
|
let M,N;
|
||
|
|
|
||
|
|
pred M beta N means
|
||
|
|
ex p st
|
||
|
|
M|p beta_shallow N|p &
|
||
|
|
for q st not p is_a_prefix_of q holds
|
||
|
|
[r,x] in M iff [r,x] in N;
|
||
|
|
end;
|
||
|
|
|
||
|
|
theorem Th4:
|
||
|
|
ProperPrefixes (v^<*x*>) = ProperPrefixes v \/ {v}
|
||
|
|
proof
|
||
|
|
thus ProperPrefixes (v^<*x*>) c= ProperPrefixes v \/ {v}
|
||
|
|
proof
|
||
|
|
let y;
|
||
|
|
assume y in ProperPrefixes (v^<*x*>);
|
||
|
|
then consider v1 such that
|
||
|
|
A1: y = v1 and
|
||
|
|
A2: v1 is_a_proper_prefix_of v^<*x*> by TREES_1:def 2;
|
||
|
|
v1 is_a_prefix_of v & v1 <> v or v1 = v by A2,TREES_1:9;
|
||
|
|
then
|
||
|
|
v1 is_a_proper_prefix_of v or v1 in {v} by TARSKI:def 1,XBOOLE_0:def 8;
|
||
|
|
then y in ProperPrefixes v or y in {v} by A1,TREES_1:def 2;
|
||
|
|
hence thesis by XBOOLE_0:def 3;
|
||
|
|
end;
|
||
|
|
let y;
|
||
|
|
assume y in ProperPrefixes v \/ {v};
|
||
|
|
then A3: y in ProperPrefixes v or y in {v} by XBOOLE_0:def 3;
|
||
|
|
A4: now
|
||
|
|
assume y in ProperPrefixes v;
|
||
|
|
then consider v1 such that
|
||
|
|
A5: y = v1 and
|
||
|
|
A6: v1 is_a_proper_prefix_of v by TREES_1:def 2;
|
||
|
|
v is_a_prefix_of v^<*x*> by TREES_1:1;
|
||
|
|
then v1 is_a_proper_prefix_of v^<*x*> by A6,XBOOLE_1:58;
|
||
|
|
hence thesis by A5,TREES_1:def 2;
|
||
|
|
end;
|
||
|
|
v^{} = v by FINSEQ_1:34;
|
||
|
|
then
|
||
|
|
v is_a_prefix_of v^<*x*> & v <> v^<*x*> by FINSEQ_1:33,TREES_1:1;
|
||
|
|
then v is_a_proper_prefix_of v^<*x*> by XBOOLE_0:def 8;
|
||
|
|
then y in ProperPrefixes v or y = v & v in ProperPrefixes (v^<*x*>)
|
||
|
|
by A3,TARSKI:def 1,TREES_1:def 2;
|
||
|
|
hence thesis by A4;
|
||
|
|
end;
|