set X = TrivialInfiniteTree ;
0 |-> 0 in TrivialInfiniteTree ;
hence not TrivialInfiniteTree is empty ; :: thesis: TrivialInfiniteTree is Tree-like
thus TrivialInfiniteTree c= NAT * :: according to TREES_1:def 3 :: thesis: ( ( for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree ) & ( for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in TrivialInfiniteTree or x in NAT * )
assume x in TrivialInfiniteTree ; :: thesis: x in NAT *
then ex k being Nat st x = k |-> 0 ;
hence x in NAT * by FINSEQ_1:def 11; :: thesis: verum
end;
thus for p being FinSequence of NAT st p in TrivialInfiniteTree holds
ProperPrefixes p c= TrivialInfiniteTree :: thesis: for p being FinSequence of NAT
for k, n being Nat st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree
proof
let p be FinSequence of NAT ; :: thesis: ( p in TrivialInfiniteTree implies ProperPrefixes p c= TrivialInfiniteTree )
assume p in TrivialInfiniteTree ; :: thesis: ProperPrefixes p c= TrivialInfiniteTree
then consider m being Nat such that
A1: p = m |-> 0 ;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ProperPrefixes p or x in TrivialInfiniteTree )
assume A2: x in ProperPrefixes p ; :: thesis: x in TrivialInfiniteTree
then reconsider x = x as FinSequence by Th10;
A3: for k being Nat st 1 <= k & k <= len x holds
x . k = ((len x) |-> 0) . k
proof
x is_a_proper_prefix_of p by A2, Th11;
then A4: x c= p ;
let k be Nat; :: thesis: ( 1 <= k & k <= len x implies x . k = ((len x) |-> 0) . k )
assume ( 1 <= k & k <= len x ) ; :: thesis: x . k = ((len x) |-> 0) . k
then A5: k in dom x by FINSEQ_3:25;
thus ((len x) |-> 0) . k = 0
.= p . k by A1
.= x . k by A5, A4, GRFUNC_1:2 ; :: thesis: verum
end;
len x = len ((len x) |-> 0) by CARD_1:def 7;
then x = (len x) |-> 0 by A3, FINSEQ_1:14;
hence x in TrivialInfiniteTree ; :: thesis: verum
end;
let p be FinSequence of NAT ; :: thesis: for k, n being Nat st p ^ <*k*> in TrivialInfiniteTree & n <= k holds
p ^ <*n*> in TrivialInfiniteTree
let m, n be Nat; :: thesis: ( p ^ <*m*> in TrivialInfiniteTree & n <= m implies p ^ <*n*> in TrivialInfiniteTree )
assume p ^ <*m*> in TrivialInfiniteTree ; :: thesis: ( not n <= m or p ^ <*n*> in TrivialInfiniteTree )
then consider k being Nat such that
A6: p ^ <*m*> = k |-> 0 ;
assume A7: n <= m ; :: thesis: p ^ <*n*> in TrivialInfiniteTree
len (p ^ <*m*>) = (len p) + 1 by FINSEQ_2:16;
then (p ^ <*m*>) . (len (p ^ <*m*>)) = m by FINSEQ_1:42;
then A8: m = 0 by A6;
A9: for z being Nat st 1 <= z & z <= len (p ^ <*n*>) holds
((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z
proof
let z be Nat; :: thesis: ( 1 <= z & z <= len (p ^ <*n*>) implies ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z )
assume ( 1 <= z & z <= len (p ^ <*n*>) ) ; :: thesis: ((len (p ^ <*n*>)) |-> 0) . z = (p ^ <*n*>) . z
thus ((len (p ^ <*n*>)) |-> 0) . z = 0
.= (p ^ <*m*>) . z by A6
.= (p ^ <*n*>) . z by A7, A8 ; :: thesis: verum
end;
len (p ^ <*n*>) = len ((len (p ^ <*n*>)) |-> 0) by CARD_1:def 7;
then (len (p ^ <*n*>)) |-> 0 = p ^ <*n*> by A9, FINSEQ_1:14;
hence p ^ <*n*> in TrivialInfiniteTree ; :: thesis: verum