:: AMISTD_3 semantic presentation

registration
let c1 be set ;
let c2 be PartFunc of c1, NAT ;
let c3 be set ;
cluster a2 . a3 -> natural ;
coherence
c2 . c3 is natural
proof
per cases not ( not c3 in dom c2 & c3 in dom c2 ) ;
suppose c3 in dom c2 ;
then reconsider c4 = c2 . c3 as Nat by PARTFUN1:27;
c4 is natural ;
hence c2 . c3 is natural ;
end;
suppose not c3 in dom c2 ;
hence c2 . c3 is natural by FUNCT_1:def 4;
end;
end;
end;
end;

registration
let c1 be empty Relation;
let c2 be set ;
cluster a1 | a2 -> empty ;
coherence
c1 | c2 is empty
proof
dom c1 misses c2 by XBOOLE_1:65;
hence c1 | c2 is empty by RELAT_1:95;
end;
end;

theorem E1: :: AMISTD_3:1
for b1, b2 being set
for b3 being Relation holds
( ( dom b3 = {b1} & rng b3 = {b2} ) implies ( b3 = b1 .--> b2 ) )
proof
let c1, c2 be set ;
let c3 be Relation;
assume that
E2: dom c3 = {c1} and
E3: rng c3 = {c2} ;
set c4 = c1 .--> c2;
E4: c1 .--> c2 = {[c1,c2]} by AMI_1:19;
for b1, b2 being set holds
( [b1,b2] in c3 iff [b1,b2] in c1 .--> c2 )
proof
let c5, c6 be set ;
hereby
assume [c5,c6] in c3 ;
then ( c5 in dom c3 & c6 in rng c3 ) by RELAT_1:20;
then ( c5 = c1 & c6 = c2 ) by E2, E3, TARSKI:def 1;
hence [c5,c6] in c1 .--> c2 by E4, TARSKI:def 1;
end;
assume [c5,c6] in c1 .--> c2 ;
then [c5,c6] = [c1,c2] by E4, TARSKI:def 1;
then E5: ( c5 = c1 & c6 = c2 ) by ZFMISC_1:33;
then c5 in dom c3 by E2, TARSKI:def 1;
then consider c7 being set such that
E6: [c5,c7] in c3 by RELAT_1:def 4;
c7 in rng c3 by E6, RELAT_1:20;
hence [c5,c6] in c3 by E3, E5, E6, TARSKI:def 1;
end;
hence c3 = c1 .--> c2 by RELAT_1:def 2;
end;

theorem E2: :: AMISTD_3:2
for b1 being set holds field {[b1,b1]} = {b1}
proof
let c1 be set ;
thus field {[c1,c1]} = {c1,c1} by RELAT_1:32
.= {c1} by ENUMSET1:69 ;
end;

registration
let c1 be infinite set ;
let c2 be set ;
cluster a1 --> a2 -> infinite ;
coherence
not c1 --> c2 is finite
proof
assume c1 --> c2 is finite ;
then reconsider c3 = c1 --> c2 as finite Relation ;
dom c3 is finite ;
hence not verum by FUNCOP_1:19;
end;
end;

registration
cluster infinite set ;
existence
not for b1 being Function holds b1 is finite
proof
take NAT --> 0 ;
thus not NAT --> 0 is finite ;
end;
end;

registration
let c1 be finite Relation;
cluster field a1 -> finite ;
coherence
field c1 is finite
proof
field c1 = (dom c1) \/ (rng c1) by RELAT_1:def 6;
hence field c1 is finite ;
end;
end;

theorem E3: :: AMISTD_3:3
for b1 being Relation holds
( field b1 is finite implies b1 is finite )
proof
let c1 be Relation;
assume field c1 is finite ;
then reconsider c2 = field c1 as finite set ;
c1 c= [:c2,c2:] by ORDERS_1:180;
hence c1 is finite by FINSET_1:13;
end;

registration
let c1 be infinite Relation;
cluster field a1 -> infinite ;
coherence
not field c1 is finite by E3;
end;

theorem :: AMISTD_3:4
for b1 being Relation holds
( ( dom b1 is finite & rng b1 is finite ) implies ( b1 is finite ) )
proof
let c1 be Relation;
assume ( dom c1 is finite & rng c1 is finite ) ;
then (dom c1) \/ (rng c1) is finite by FINSET_1:14;
then field c1 is finite by RELAT_1:def 6;
hence c1 is finite by E3;
end;

registration
cluster RelIncl {} -> empty ;
coherence
RelIncl {} is empty
proof
for b1, b2 being set holds
( ( b1 in {} & b2 in {} ) implies ( ( [b1,b2] in {} iff b1 c= b2 ) ) ) ;
hence RelIncl {} is empty by TOLER_1:1, WELLORD2:def 1;
end;
end;

registration
let c1 be non empty set ;
cluster RelIncl a1 -> non empty ;
coherence
not RelIncl c1 is empty
proof
consider c2 being Element of c1;
[c2,c2] in RelIncl c1 by WELLORD2:def 1;
hence not RelIncl c1 is empty ;
end;
end;

theorem E4: :: AMISTD_3:5
for b1 being set holds RelIncl {b1} = {[b1,b1]}
proof
let c1 be set ;
E5: field {[c1,c1]} = {c1} by E2;
for b1, b2 being set holds
( ( b1 in {c1} & b2 in {c1} ) implies ( ( [b1,b2] in {[c1,c1]} iff b1 c= b2 ) ) )
proof
let c2, c3 be set ;
assume ( c2 in {c1} & c3 in {c1} ) ;
then E6: ( c2 = c1 & c3 = c1 ) by TARSKI:def 1;
hence ( [c2,c3] in {[c1,c1]} implies c2 c= c3 ) ;
thus ( c2 c= c3 implies [c2,c3] in {[c1,c1]} ) by E6, TARSKI:def 1;
end;
hence RelIncl {c1} = {[c1,c1]} by E5, WELLORD2:def 1;
end;

theorem E5: :: AMISTD_3:6
for b1 being set holds RelIncl b1 c= [:b1,b1:]
proof
let c1 be set ;
set c2 = RelIncl c1;
let c3 be set ; :: according to TARSKI:def 3
assume E6: c3 in RelIncl c1 ;
then consider c4, c5 being set such that
E7: c3 = [c4,c5] by RELAT_1:def 1;
( c4 in field (RelIncl c1) & c5 in field (RelIncl c1) ) by E6, E7, RELAT_1:30;
then ( c4 in c1 & c5 in c1 ) by WELLORD2:def 1;
hence c3 in [:c1,c1:] by E7, ZFMISC_1:106;
end;

registration
let c1 be finite set ;
cluster RelIncl a1 -> finite ;
coherence
RelIncl c1 is finite
proof
RelIncl c1 c= [:c1,c1:] by E5;
hence RelIncl c1 is finite by FINSET_1:13;
end;
end;

theorem E6: :: AMISTD_3:7
for b1 being set holds
( RelIncl b1 is finite implies b1 is finite )
proof
let c1 be set ;
set c2 = RelIncl c1;
assume RelIncl c1 is finite ;
then reconsider c3 = RelIncl c1 as finite Relation ;
field c3 is finite ;
hence c1 is finite by WELLORD2:def 1;
end;

registration
let c1 be infinite set ;
cluster RelIncl a1 -> non empty infinite ;
coherence
not RelIncl c1 is finite by E6;
end;

theorem :: AMISTD_3:8
for b1, b2 being Relation holds
( ( b1,b2 are_isomorphic & b1 is well-ordering ) implies ( b2 is well-ordering ) )
proof
let c1, c2 be Relation;
assume c1,c2 are_isomorphic ;
then ex b1 being Function st b1 is_isomorphism_of c1,c2 by WELLORD1:def 8;
hence not ( c1 is well-ordering & not c2 is well-ordering ) by WELLORD1:54;
end;

theorem E7: :: AMISTD_3:9
for b1, b2 being Relation holds
( ( b1,b2 are_isomorphic & b1 is finite ) implies ( b2 is finite ) )
proof
let c1, c2 be Relation;
given c3 being Function such that E8: c3 is_isomorphism_of c1,c2 ; :: according to WELLORD1:def 8
assume c1 is finite ;
then reconsider c4 = c1 as finite Relation ;
field c4 is finite ;
then dom c3 is finite by E8, WELLORD1:def 7;
then rng c3 is finite by FINSET_1:26;
then field c2 is finite by E8, WELLORD1:def 7;
hence c2 is finite by E3;
end;

theorem E8: :: AMISTD_3:10
for b1, b2 being set holds b1 .--> b2 is_isomorphism_of {[b1,b1]},{[b2,b2]}
proof
let c1, c2 be set ;
set c3 = c1 .--> c2;
set c4 = {[c1,c1]};
set c5 = {[c2,c2]};
E9: field {[c1,c1]} = {c1} by E2;
hence dom (c1 .--> c2) = field {[c1,c1]} by CQC_LANG:5; :: according to WELLORD1:def 7
field {[c2,c2]} = {c2} by E2;
hence rng (c1 .--> c2) = field {[c2,c2]} by CQC_LANG:5;
thus c1 .--> c2 is one-to-one ;
let c6, c7 be set ;
hereby
assume [c6,c7] in {[c1,c1]} ;
then [c6,c7] = [c1,c1] by TARSKI:def 1;
then E10: ( c6 = c1 & c7 = c1 ) by ZFMISC_1:33;
hence ( c6 in field {[c1,c1]} & c7 in field {[c1,c1]} ) by E9, TARSKI:def 1;
(c1 .--> c2) . c1 = c2 by CQC_LANG:6;
hence [((c1 .--> c2) . c6),((c1 .--> c2) . c7)] in {[c2,c2]} by E10, TARSKI:def 1;
end;
assume ( c6 in field {[c1,c1]} & c7 in field {[c1,c1]} ) ;
then ( c6 = c1 & c7 = c1 ) by E9, TARSKI:def 1;
hence not ( [((c1 .--> c2) . c6),((c1 .--> c2) . c7)] in {[c2,c2]} & not [c6,c7] in {[c1,c1]} ) by TARSKI:def 1;
end;

theorem :: AMISTD_3:11
for b1, b2 being set holds {[b1,b1]},{[b2,b2]} are_isomorphic
proof
let c1, c2 be set ;
take c3 = c1 .--> c2; :: according to WELLORD1:def 8
thus c3 is_isomorphism_of {[c1,c1]},{[c2,c2]} by E8;
end;

registration
cluster order_type_of {} -> empty ;
coherence
order_type_of {} is empty
proof
{} , RelIncl {} are_isomorphic by WELLORD1:48;
hence order_type_of {} is empty by ORDERS_1:119, WELLORD2:def 2;
end;
end;

theorem :: AMISTD_3:12
for b1 being Ordinal holds order_type_of (RelIncl b1) = b1
proof
let c1 be Ordinal;
E9: RelIncl c1 is well-ordering by WELLORD2:7;
RelIncl c1, RelIncl c1 are_isomorphic by WELLORD1:48;
hence order_type_of (RelIncl c1) = c1 by E9, WELLORD2:def 2;
end;

E9: for b1 being Ordinal
for b2 being finite set holds
( b2 c= b1 implies order_type_of (RelIncl b2) is finite )
proof
let c1 be Ordinal;
let c2 be finite set ;
assume c2 c= c1 ;
then RelIncl c2 is well-ordering by WELLORD2:9;
then RelIncl c2, RelIncl (order_type_of (RelIncl c2)) are_isomorphic by WELLORD2:def 2;
then RelIncl (order_type_of (RelIncl c2)) is finite by E7;
hence order_type_of (RelIncl c2) is finite by E6;
end;

theorem E10: :: AMISTD_3:13
for b1 being Ordinal
for b2 being finite set holds
( b2 c= b1 implies order_type_of (RelIncl b2) = card b2 )
proof
let c1 be Ordinal;
let c2 be finite set ;
assume E11: c2 c= c1 ;
then E12: card c2 = Card (order_type_of (RelIncl c2)) by CARD_5:16;
order_type_of (RelIncl c2) is finite by E11, E9;
then order_type_of (RelIncl c2) in omega by CARD_4:7;
hence order_type_of (RelIncl c2) = card c2 by E12, CARD_1:66;
end;

theorem E11: :: AMISTD_3:14
for b1 being set
for b2 being Ordinal holds
( {b1} c= b2 implies order_type_of (RelIncl {b1}) = 1 )
proof
let c1 be set ;
let c2 be Ordinal;
card {c1} = 1 by CARD_2:60;
hence ( {c1} c= c2 implies order_type_of (RelIncl {c1}) = 1 ) by E10;
end;

theorem E12: :: AMISTD_3:15
for b1 being set
for b2 being Ordinal holds
( {b1} c= b2 implies canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {b1}))),(RelIncl {b1}) = 0 .--> b1 )
proof
let c1 be set ;
let c2 be Ordinal;
set c3 = {c1};
set c4 = RelIncl {c1};
set c5 = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {c1}))),(RelIncl {c1});
assume E13: {c1} c= c2 ;
then RelIncl {c1} is well-ordering by WELLORD2:9;
then RelIncl {c1}, RelIncl (order_type_of (RelIncl {c1})) are_isomorphic by WELLORD2:def 2;
then E14: RelIncl (order_type_of (RelIncl {c1})), RelIncl {c1} are_isomorphic by WELLORD1:50;
RelIncl (order_type_of (RelIncl {c1})) is well-ordering by WELLORD2:9;
then E15: canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {c1}))),(RelIncl {c1}) is_isomorphism_of RelIncl (order_type_of (RelIncl {c1})), RelIncl {c1} by E14, WELLORD1:def 9;
E16: RelIncl {0} = {[0,0]} by E4;
E17: order_type_of (RelIncl {c1}) = {0} by E13, E11, CARD_5:1;
then E18: dom (canonical_isomorphism_of (RelIncl {0}),(RelIncl {c1})) = field (RelIncl {0}) by E15, WELLORD1:def 7
.= {0} by E16, E2 ;
rng (canonical_isomorphism_of (RelIncl {0}),(RelIncl {c1})) = field (RelIncl {c1}) by E15, E17, WELLORD1:def 7
.= {c1} by WELLORD2:def 1 ;
hence canonical_isomorphism_of (RelIncl (order_type_of (RelIncl {c1}))),(RelIncl {c1}) = 0 .--> c1 by E17, E18, E1;
end;

registration
let c1 be Ordinal;
let c2 be Subset of c1;
let c3 be set ;
cluster (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl a2))),(RelIncl a2)) . a3 -> ordinal ;
coherence
(canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c2))),(RelIncl c2)) . c3 is ordinal
proof
consider c4 being Ordinal-Sequence such that
E13: ( c4 = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c2))),(RelIncl c2) & c4 is increasing & dom c4 = order_type_of (RelIncl c2) ) and
E14: rng c4 = c2 by CARD_5:14;
per cases not ( not c3 in dom c4 & c3 in dom c4 ) ;
suppose c3 in dom c4 ;
then c4 . c3 in rng c4 by FUNCT_1:def 5;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c2))),(RelIncl c2)) . c3 is ordinal by E13, E14, ORDINAL1:23;
end;
suppose not c3 in dom c4 ;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c2))),(RelIncl c2)) . c3 is ordinal by E13, FUNCT_1:def 4;
end;
end;
end;
end;

registration
let c1 be natural-membered set ;
let c2 be set ;
cluster (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl a1))),(RelIncl a1)) . a2 -> natural ;
coherence
(canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c1))),(RelIncl c1)) . c2 is natural
proof
c1 c= NAT
proof
let c3 be set ; :: according to TARSKI:def 3
assume c3 in c1 ;
then c3 is natural by MEMBERED:def 5;
hence c3 in NAT by ORDINAL2:def 21;
end;
then reconsider c3 = c1 as Subset of NAT ;
consider c4 being Ordinal-Sequence such that
E13: ( c4 = canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c3))),(RelIncl c3) & c4 is increasing & dom c4 = order_type_of (RelIncl c3) ) and
E14: rng c4 = c3 by CARD_5:14;
per cases not ( not c2 in dom c4 & c2 in dom c4 ) ;
suppose E15: c2 in dom c4 ;
then E16: c4 . c2 in rng c4 by FUNCT_1:def 5;
reconsider c5 = c4 . c2 as Element of c3 by E14, E15, FUNCT_1:def 5;
c5 is Nat by E14, E16;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c1))),(RelIncl c1)) . c2 is natural by E13;
end;
suppose not c2 in dom c4 ;
hence (canonical_isomorphism_of (RelIncl (order_type_of (RelIncl c1))),(RelIncl c1)) . c2 is natural by E13, FUNCT_1:def 4;
end;
end;
end;
end;

theorem E13: :: AMISTD_3:16
for b1 being set
for b2, b3 being natural number holds
( b2 |-> b1 = b3 |-> b1 implies b2 = b3 )
proof
let c1 be set ;
let c2, c3 be natural number ;
( len (c2 |-> c1) = c2 & len (c3 |-> c1) = c3 ) by FINSEQ_2:69;
hence ( c2 |-> c1 = c3 |-> c1 implies c2 = c3 ) ;
end;

theorem E14: :: AMISTD_3:17
for b1 being natural number
for b2 being Tree
for b3 being Element of b2 holds b3 | (Seg b1) in b2
proof
let c1 be natural number ;
let c2 be Tree;
let c3 be Element of c2;
c3 | (Seg c1) is_a_prefix_of c3 by RELAT_1:88;
hence c3 | (Seg c1) in c2 by TREES_1:45;
end;

theorem E15: :: AMISTD_3:18
for b1, b2 being Tree holds
( ( for b3 being Nat holds b1 -level b3 = b2 -level b3 ) implies b1 = b2 )
proof
let c1, c2 be Tree;
assume E16: for b1 being Nat holds c1 -level b1 = c2 -level b1 ;
for b1 being FinSequence of NAT holds
( b1 in c1 iff b1 in c2 )
proof
let c3 be FinSequence of NAT ;
E17: c1 = union { (c1 -level b1) where B is Nat : verum } by TREES_2:16;
E18: c2 = union { (c2 -level b1) where B is Nat : verum } by TREES_2:16;
hereby
assume c3 in c1 ;
then consider c4 being set such that
E19: c3 in c4 and
E20: c4 in { (c1 -level b1) where B is Nat : verum } by E17, TARSKI:def 4;
consider c5 being Nat such that
E21: c4 = c1 -level c5 by E20;
c4 = c2 -level c5 by E16, E21;
hence c3 in c2 by E19;
end;
assume c3 in c2 ;
then consider c4 being set such that
E19: c3 in c4 and
E20: c4 in { (c2 -level b1) where B is Nat : verum } by E18, TARSKI:def 4;
consider c5 being Nat such that
E21: c4 = c2 -level c5 by E20;
c4 = c1 -level c5 by E16, E21;
hence c3 in c1 by E19;
end;
hence c1 = c2 by TREES_2:7;
end;

definition
func TrivialInfiniteTree -> set equals :: AMISTD_3:def 1
{ (b1 |-> 0) where B is Nat : verum } ;
coherence
{ (b1 |-> 0) where B is Nat : verum } is set ;
end;

:: deftheorem defines TrivialInfiniteTree AMISTD_3:def 1 :
TrivialInfiniteTree = { (b1 |-> 0) where B is Nat : verum } ;

registration
cluster TrivialInfiniteTree -> non empty Tree-like ;
coherence
( not TrivialInfiniteTree is empty & TrivialInfiniteTree is Tree-like )
proof
set c1 = TrivialInfiniteTree ;
0 |-> 0 in TrivialInfiniteTree ;
hence not TrivialInfiniteTree is empty ;
thus TrivialInfiniteTree c= NAT * :: according to TREES_1:def 5
proof
let c2 be set ; :: according to TARSKI:def 3
assume c2 in TrivialInfiniteTree ;
then ex b1 being Nat st c2 = b1 |-> 0 ;
then c2 is FinSequence of NAT by FINSEQ_2:77;
hence c2 in NAT * by FINSEQ_1:def 11;
end;
thus for b1 being FinSequence of NAT holds
( b1 in TrivialInfiniteTree implies ProperPrefixes b1 c= TrivialInfiniteTree )
proof
let c2 be FinSequence of NAT ;
assume c2 in TrivialInfiniteTree ;
then consider c3 being Nat such that
E16: c2 = c3 |-> 0 ;
let c4 be set ; :: according to TARSKI:def 3
assume E17: c4 in ProperPrefixes c2 ;
then reconsider c5 = c4 as FinSequence by TREES_1:35;
E18: len c5 = len ((len c5) |-> 0) by FINSEQ_2:69;
for b1 being Nat holds
( ( 1 <= b1 & b1 <= len c5 ) implies ( c5 . b1 = ((len c5) |-> 0) . b1 ) )
proof
let c6 be Nat;
assume ( 1 <= c6 & c6 <= len c5 ) ;
then E19: c6 in dom c5 by FINSEQ_3:27;
then E20: c6 in Seg (len c5) by FINSEQ_1:def 3;
len c5 < len c2 by E17, TREES_1:37;
then Seg (len c5) c= Seg (len c2) by FINSEQ_1:7;
then c6 in Seg (len c2) by E20;
then E21: c6 in Seg c3 by E16, FINSEQ_2:69;
c5 is_a_proper_prefix_of c2 by E17, TREES_1:36;
then E22: c5 c= c2 by XBOOLE_0:def 8;
thus ((len c5) |-> 0) . c6 = 0 by E20, FINSEQ_2:70
.= c2 . c6 by E16, E21, FINSEQ_2:70
.= c5 . c6 by E19, E22, GRFUNC_1:8 ;
end;
then c5 = (len c5) |-> 0 by E18, FINSEQ_1:18;
hence c4 in TrivialInfiniteTree ;
end;
let c2 be FinSequence of NAT ;
let c3, c4 be Nat;
assume c2 ^ <*c3*> in TrivialInfiniteTree ;
then consider c5 being Nat such that
E16: c2 ^ <*c3*> = c5 |-> 0 ;
assume E17: c4 <= c3 ;
E18: len (c2 ^ <*c3*>) = (len c2) + 1 by FINSEQ_2:19;
E19: len (c2 ^ <*c3*>) = c5 by E16, FINSEQ_2:69;
E20: (c2 ^ <*c3*>) . (len (c2 ^ <*c3*>)) = c3 by E18, FINSEQ_1:59;
not ( not 0 = c5 & not 0 < c5 ) ;
then 0 + 1 <= c5 by E16, FINSEQ_2:72, NAT_1:38;
then c5 in Seg c5 by FINSEQ_1:3;
then E21: c3 = 0 by E16, E19, E20, FINSEQ_2:70;
E22: len (c2 ^ <*c4*>) = len ((len (c2 ^ <*c4*>)) |-> 0) by FINSEQ_2:69;
for b1 being Nat holds
( ( 1 <= b1 & b1 <= len (c2 ^ <*c4*>) ) implies ( ((len (c2 ^ <*c4*>)) |-> 0) . b1 = (c2 ^ <*c4*>) . b1 ) )
proof
let c6 be Nat;
assume that
E23: 1 <= c6 and
E24: c6 <= len (c2 ^ <*c4*>) ;
c6 in dom (c2 ^ <*c4*>) by E23, E24, FINSEQ_3:27;
then E25: c6 in Seg (len (c2 ^ <*c4*>)) by FINSEQ_1:def 3;
len (c2 ^ <*c4*>) = (len c2) + 1 by FINSEQ_2:19;
then E26: c6 in Seg c5 by E18, E19, E23, E24, FINSEQ_1:3;
thus ((len (c2 ^ <*c4*>)) |-> 0) . c6 = 0 by E25, FINSEQ_2:70
.= (c2 ^ <*c3*>) . c6 by E16, E26, FINSEQ_2:70
.= (c2 ^ <*c4*>) . c6 by E17, E21, NAT_1:19 ;
end;
then (len (c2 ^ <*c4*>)) |-> 0 = c2 ^ <*c4*> by E22, FINSEQ_1:18;
hence c2 ^ <*c4*> in TrivialInfiniteTree ;
end;
end;

theorem E16: :: AMISTD_3:19
NAT , TrivialInfiniteTree are_equipotent
proof
defpred S1[ Nat, set ] means a2 = a1 |-> 0;
E17: for b1 being Element of NAT holds
ex b2 being Element of TrivialInfiniteTree st
S1[b1,b2]
proof
let c1 be Element of NAT ;
c1 |-> 0 in TrivialInfiniteTree ;
then reconsider c2 = c1 |-> 0 as Element of TrivialInfiniteTree ;
take c2 ;
thus S1[c1,c2] ;
end;
consider c1 being Function of NAT , TrivialInfiniteTree such that
E18: for b1 being Element of NAT holds
S1[b1,c1 . b1] from FUNCT_2:sch 3(E17);
 take c1 ; :: according to WELLORD2:def 4
thus c1 is one-to-one
proof
let c2, c3 be set ; :: according to FUNCT_1:def 8
assume E19: ( c2 in dom c1 & c3 in dom c1 ) ;
assume E20: c1 . c2 = c1 . c3 ;
reconsider c4 = c2, c5 = c3 as Nat by E19, FUNCT_2:def 1;
( S1[c4,c1 . c4] & S1[c5,c1 . c5] ) by E18;
hence c2 = c3 by E20, E13;
end;
thus E19: dom c1 = NAT by FUNCT_2:def 1;
thus rng c1 c= TrivialInfiniteTree by RELSET_1:12; :: according to XBOOLE_0:def 10
let c2 be set ; :: according to TARSKI:def 3
assume c2 in TrivialInfiniteTree ;
then consider c3 being Nat such that
E20: c2 = c3 |-> 0 ;
( c3 in dom c1 & c1 . c3 = c2 ) by E18, E19, E20;
hence c2 in rng c1 by FUNCT_1:def 5;
end;

registration
cluster TrivialInfiniteTree -> non empty infinite Tree-like ;
coherence
not TrivialInfiniteTree is finite by E16, CARD_1:68;
end;

theorem E17: :: AMISTD_3:20
for b1 being Nat holds TrivialInfiniteTree -level b1 = {(b1 |-> 0)}
proof
let c1 be Nat;
set c2 = TrivialInfiniteTree ;
set c3 = { b1 where B is Element of TrivialInfiniteTree : len b1 = c1 } ;
set c4 = c1 |-> 0;
{(c1 |-> 0)} = { b1 where B is Element of TrivialInfiniteTree : len b1 = c1 }
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10
let c5 be set ;
assume c5 in {(c1 |-> 0)} ;
then E18: c5 = c1 |-> 0 by TARSKI:def 1;
E19: c1 |-> 0 in TrivialInfiniteTree ;
len (c1 |-> 0) = c1 by FINSEQ_2:69;
hence c5 in { b1 where B is Element of TrivialInfiniteTree : len b1 = c1 } by E18, E19;
end;
let c5 be set ; :: according to TARSKI:def 3
assume c5 in { b1 where B is Element of TrivialInfiniteTree : len b1 = c1 } ;
then consider c6 being Element of TrivialInfiniteTree such that
E18: ( c5 = c6 & len c6 = c1 ) ;
c6 in TrivialInfiniteTree ;
then ex b1 being Nat st c6 = b1 |-> 0 ;
then c5 = c1 |-> 0 by E18, FINSEQ_2:69;
hence c5 in {(c1 |-> 0)} by TARSKI:def 1;
end;
hence TrivialInfiniteTree -level c1 = {(c1 |-> 0)} by TREES_2:def 6;
end;

definition
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite standard AMI-Struct of c1;
let c3 be FinPartState of c2;
assume that
E18: not c3 is empty and
E19: c3 is programmed ;
func FirstLoc c3 -> Instruction-Location of a2 means :E18: :: AMISTD_3:def 2
ex b1 being non empty Subset of NAT st
( b1 = { (locnum b2) where B is Element of the Instruction-Locations of a2 : b2 in dom a3 } & a4 = il. a2,(min b1) );
existence
ex b1 being Instruction-Location of c2ex b2 being non empty Subset of NAT st
( b2 = { (locnum b3) where B is Element of the Instruction-Locations of c2 : b3 in dom c3 } & b1 = il. c2,(min b2) )
proof
deffunc H1( Element of the Instruction-Locations of c2) -> Element of NAT = locnum a1;
reconsider c4 = c3 as non empty programmed FinPartState of c2 by E18, E19;
set c5 = { H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } ;
E20: dom c4 is finite ;
E21: { H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } is finite from FRAENKEL:sch 21(E20);
 consider c6 being Element of dom c4;
( c6 in dom c4 & dom c4 c= the Instruction-Locations of c2 ) by AMI_3:def 13;
then reconsider c7 = c6 as Element of the Instruction-Locations of c2 ;
E22: locnum c7 in { H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } ;
{ H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } c= NAT
proof
let c8 be set ; :: according to TARSKI:def 3
assume c8 in { H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } ;
then ex b1 being Element of the Instruction-Locations of c2 st
( c8 = locnum b1 & b1 in dom c4 ) ;
hence c8 in NAT ;
end;
then reconsider c8 = { H1(b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c4 } as non empty finite Subset of NAT by E21, E22;
take il. c2,(min c8) ;
take c8 ;
thus ( c8 = { (locnum b1) where B is Element of the Instruction-Locations of c2 : b1 in dom c3 } & il. c2,(min c8) = il. c2,(min c8) ) ;
end;
uniqueness
for b1, b2 being Instruction-Location of c2 holds
( ( ) implies ( ( for b3 being non empty Subset of NAT holds
not ( b3 = { (locnum b4) where B is Element of the Instruction-Locations of c2 : b4 in dom c3 } & b1 = il. c2,(min b3) ) ) or ( for b3 being non empty Subset of NAT holds
not ( b3 = { (locnum b4) where B is Element of the Instruction-Locations of c2 : b4 in dom c3 } & b2 = il. c2,(min b3) ) ) or b1 = b2 ) ) ;
end;

:: deftheorem E18 defines FirstLoc AMISTD_3:def 2 :
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being FinPartState of b2 holds
( ( b3 is programmed ) implies ( b3 is empty or ( for b4 being Instruction-Location of b2 holds
( b4 = FirstLoc b3 iff ex b5 being non empty Subset of NAT st
( b5 = { (locnum b6) where B is Element of the Instruction-Locations of b2 : b6 in dom b3 } & b4 = il. b2,(min b5) ) ) ) ) );

theorem E19: :: AMISTD_3:21
for b1 being with_non-empty_elements set
for b2 being non empty non void IC-Ins-separated definite standard AMI-Struct of b1
for b3 being non empty programmed FinPartState of b2 holds FirstLoc b3 in dom b3
proof
let c1 be with_non-empty_elements set ;
let c2 be non empty non void IC-Ins-separated definite standard AMI-Struct of c1;
let c3 be non empty programmed FinPartState of c2;
consider c4 being non empty Subset of NAT such that
E20: c4 = { (locnum b1) where B is Element of the Instruction-Locations of c2 : b1 in