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;
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 &
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;
end;
definition
mode LambdaTerm is LambdaTerm-like DecoratedTree of NAT;
end;
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;