:: AMISTD_2 semantic presentation

E1: for b₁ being Relation holds
not ( dom b₁ <> {} & not b₁ <> {} )
by RELAT_1:60;

registration

let c₁ be Function;
let c₂ be non empty Function;
cluster a₁ +* a₂ -> non empty ;
coherence

proof

dom (c₁ +* c₂) = (dom c₁) \/ (dom c₂) by FUNCT_4:def 1;
hence not c₁ +* c₂ is empty by E1;

end;

cluster a₂ +* a₁ -> non empty ;
coherence

proof

dom (c₂ +* c₁) = (dom c₂) \/ (dom c₁) by FUNCT_4:def 1;
hence not c₂ +* c₁ is empty by E1;

end;

registration

let c₁, c₂ be finite Function;
cluster a₁ +* a₂ -> finite ;
coherence

proof

dom (c₁ +* c₂) = (dom c₁) \/ (dom c₂) by FUNCT_4:def 1;
hence c₁ +* c₂ is finite by FINSET_1:29;

end;

theorem E2: :: AMISTD_2:1

for b₁, b₂ being Function holds
( dom b₁, dom b₂ are_equipotent iff b₁,b₂ are_equipotent )

proof

let c₁, c₂ be Function;
E3: ( Card c₁ = Card (dom c₁) & Card c₂ = Card (dom c₂) ) by PRE_CIRC:21;

hereby

assume dom c₁, dom c₂ are_equipotent ;
then Card (dom c₁) = Card (dom c₂) by CARD_1:21;
hence c₁,c₂ are_equipotent by E3, CARD_1:21;

end; assume c₁,c₂ are_equipotent ;
then Card c₁ = Card c₂ by CARD_1:21;
hence dom c₁, dom c₂ are_equipotent by E3, CARD_1:21;

end;

theorem E3: :: AMISTD_2:2

for b₁, b₂ being finite Function holds
( dom b₁ misses dom b₂ implies card (b₁ +* b₂) = (card b₁) + (card b₂) )

proof

let c₁, c₂ be finite Function;
assume E4: dom c₁ misses dom c₂ ;
thus card (c₁ +* c₂) = card (dom (c₁ +* c₂)) by PRE_CIRC:21
.= card ((dom c₁) \/ (dom c₂)) by FUNCT_4:def 1
.= (card (dom c₁)) + (card (dom c₂)) by E4, CARD_2:53
.= (card (dom c₁)) + (card c₂) by PRE_CIRC:21
.= (card c₁) + (card c₂) by PRE_CIRC:21 ;

end;

registration

let c₁ be Function;
let c₂ be set ;
cluster a₁ \ a₂ -> Relation-like Function-like ;
coherence by GRFUNC_1:38;

end;

theorem E4: :: AMISTD_2:3

for b₁ being set
for b₂, b₃ being Function holds
( b₁ in (dom b₂) \ (dom b₃) implies (b₂ \ b₃) . b₁ = b₂ . b₁ )

proof

let c₁ be set ;
let c₂, c₃ be Function;
assume E5: c₁ in (dom c₂) \ (dom c₃) ;
E6: (dom c₂) \ (dom c₃) c= dom (c₂ \ c₃) by RELAT_1:15;
c₂ \ c₃ c= c₂ by XBOOLE_1:36;
hence (c₂ \ c₃) . c₁ = c₂ . c₁ by E5, E6, GRFUNC_1:8;

end;

theorem E5: :: AMISTD_2:4

for b₁ being non empty finite set holds (card b₁) - 1 = (card b₁) -' 1

proof

let c₁ be non empty finite set ;
card c₁ <> 0 by CARD_2:59;
then card c₁ >= 1 by NAT_1:39;
then (card c₁) - 1 >= 0 by XREAL_1:50;
hence (card c₁) - 1 = (card c₁) -' 1 by BINARITH:def 3;

end;

definition

let c₁ be functional set ;
func PA a₁ -> Function means :E6: :: AMISTD_2:def 1
( for b₁ being set holds
( b₁ in dom a₂ iff for b₂ being Function holds
( b₂ in a₁ implies b₁ in dom b₂ ) ) & for b₁ being set holds
( b₁ in dom a₂ implies a₂ . b₁ = pi a₁,b₁ ) ) if not a₁ is empty
otherwise a₂ = {} ;
existence

proof

thus not ( not c₁ is empty & for b₁ being Function holds
not ( for b₂ being set holds
( b₂ in dom b₁ iff for b₃ being Function holds
( b₃ in c₁ implies b₂ in dom b₃ ) ) & for b₂ being set holds
( b₂ in dom b₁ implies b₁ . b₂ = pi c₁,b₂ ) ) )

proof

assume not c₁ is empty ;
then reconsider c₂ = c₁ as non empty functional set ;
set c₃ = { (dom b₁) where B is Element of c₂ : verum } ;
defpred S₁[ set , set ] means a₂ = pi c₁,a₁;
E6: for b₁ being set holds
not ( b₁ in meet { (dom b₂) where B is Element of c₂ : verum } & for b₂ being set holds
not S₁[b₁,b₂] ) ;
consider c₄ being Function such that
E7: dom c₄ = meet { (dom b₁) where B is Element of c₂ : verum }
and E8: for b₁ being set holds
( b₁ in meet { (dom b₂) where B is Element of c₂ : verum } implies S₁[b₁,c₄ . b₁] ) from ZFREFLE1:sch 1(E6);
take c₄ ;

hereby

let c₅ be set ;

hereby

assume E9: c₅ in dom c₄ ;
let c₆ be Function;
assume c₆ in c₁ ;
then dom c₆ in { (dom b₁) where B is Element of c₂ : verum } ;
hence c₅ in dom c₆ by E7, E9, SETFAM_1:def 1;

end;assume E9: for b₁ being Function holds
( b₁ in c₁ implies c₅ in dom b₁ ) ;
consider c₆ being Element of c₂;
E10: dom c₆ in { (dom b₁) where B is Element of c₂ : verum } ;
for b₁ being set holds
( b₁ in { (dom b₂) where B is Element of c₂ : verum } implies c₅ in b₁ )

proof

let c₇ be set ;
assume c₇ in { (dom b₁) where B is Element of c₂ : verum } ;
then ex b₁ being Element of c₂ st c₇ = dom b₁ ;
hence c₅ in c₇ by E9;

end;

hence c₅ in dom c₄ by E7, E10, SETFAM_1:def 1;

end; thus for b₁ being set holds
( b₁ in dom c₄ implies c₄ . b₁ = pi c₁,b₁ ) by E7, E8;

end;

thus not ( c₁ is empty & for b₁ being Function holds
not b₁ = {} ) ;

end;

uniqueness

proof

let c₂, c₃ be Function;
thus ( ( for b₁ being set holds
( b₁ in dom c₂ iff for b₂ being Function holds
( b₂ in c₁ implies b₁ in dom b₂ ) ) & for b₁ being set holds
( b₁ in dom c₂ implies c₂ . b₁ = pi c₁,b₁ ) & for b₁ being set holds
( b₁ in dom c₃ iff for b₂ being Function holds
( b₂ in c₁ implies b₁ in dom b₂ ) ) & for b₁ being set holds
( b₁ in dom c₃ implies c₃ . b₁ = pi c₁,b₁ ) ) implies ( c₁ is empty or c₂ = c₃ ) )

proof

defpred S₁[ set ] means for b₁ being Function holds
( b₁ in c₁ implies a₁ in dom b₁ );
assume that not c₁ is empty
and E6: for b₁ being set holds
( b₁ in dom c₂ iff S₁[b₁] )
and E7: for b₁ being set holds
( b₁ in dom c₂ implies c₂ . b₁ = pi c₁,b₁ )
and E8: for b₁ being set holds
( b₁ in dom c₃ iff S₁[b₁] )
and E9: for b₁ being set holds
( b₁ in dom c₃ implies c₃ . b₁ = pi c₁,b₁ ) ;
E10: dom c₂ = dom c₃ from XBOOLE_0:sch 2(E6, E8);

now

let c₄ be set ;
assume E11: c₄ in dom c₂ ;
hence c₂ . c₄ = pi c₁,c₄ by E7
.= c₃ . c₄ by E9, E10, E11 ;

end;

hence c₂ = c₃ by E10, FUNCT_1:9;

end;

thus ( ( c₁ is empty & c₂ = {} & c₃ = {} ) implies ( c₂ = c₃ ) ) ;

end;

consistency ;

end;

:: deftheorem E6 defines PA AMISTD_2:def 1 :

theorem :: AMISTD_2:5

for b₁ being non empty functional set holds dom (PA b₁) = meet { (dom b₂) where B is Element of b₁ : verum }

proof

let c₁ be non empty functional set ;
set c₂ = { (dom b₁) where B is Element of c₁ : verum } ;

hereby :: uses TARSKI:def 3,XBOOLE_0:def 10

let c₃ be set ;
assume E7: c₃ in dom (PA c₁) ;
consider c₄ being Element of c₁;
E8: dom c₄ in { (dom b₁) where B is Element of c₁ : verum } ;
for b₁ being set holds
( b₁ in { (dom b₂) where B is Element of c₁ : verum } implies c₃ in b₁ )

proof

let c₅ be set ;
assume c₅ in { (dom b₁) where B is Element of c₁ : verum } ;
then ex b₁ being Element of c₁ st c₅ = dom b₁ ;
hence c₃ in c₅ by E7, E6;

end;

hence c₃ in meet { (dom b₁) where B is Element of c₁ : verum } by E8, SETFAM_1:def 1;

end; let c₃ be set ; :: uses TARSKI:def 3
assume E7: c₃ in meet { (dom b₁) where B is Element of c₁ : verum } ;
for b₁ being Function holds
( b₁ in c₁ implies c₃ in dom b₁ )

proof

let c₄ be Function;
assume c₄ in c₁ ;
then dom c₄ in { (dom b₁) where B is Element of c₁ : verum } ;
hence c₃ in dom c₄ by E7, SETFAM_1:def 1;

end;

hence c₃ in dom (PA c₁) by E6;

end;

theorem :: AMISTD_2:6

for b₁ being non empty functional set
for b₂ being set holds
( b₂ in dom (PA b₁) implies (PA b₁) . b₂ = { (b₃ . b₂) where B is Element of b₁ : verum } )

proof

let c₁ be non empty functional set ;
let c₂ be set ;
assume E7: c₂ in dom (PA c₁) ;

hereby :: uses TARSKI:def 3,XBOOLE_0:def 10

let c₃ be set ;
assume c₃ in (PA c₁) . c₂ ;
then c₃ in pi c₁,c₂ by E7, E6;
then ex b₁ being Function st
( b₁ in c₁ & c₃ = b₁ . c₂ ) by CARD_3:def 6;
hence c₃ in { (b₁ . c₂) where B is Element of c₁ : verum } ;

end; let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in { (b₁ . c₂) where B is Element of c₁ : verum } ;
then ex b₁ being Element of c₁ st c₃ = b₁ . c₂ ;
then c₃ in pi c₁,c₂ by CARD_3:def 6;
hence c₃ in (PA c₁) . c₂ by E7, E6;

end;

definition

let c₁ be set ;
attr a₁ is product-like means :E7: :: AMISTD_2:def 2
ex b₁ being Function st a₁ = product b₁;

end;

:: deftheorem E7 defines product-like AMISTD_2:def 2 :

registration

let c₁ be Function;
cluster product a₁ -> product-like ;
coherence by E7;

end;

registration

cluster product-like -> functional with_common_domain set ;
coherence

proof

let c₁ be set ;
given c₂ being Function such that E8: c₁ = product c₂ ; :: uses AMISTD_2:def 2
thus c₁ is functional by E8;
let c₃, c₄ be Function; :: uses PRALG_2:def 1
assume that E9: c₃ in c₁
and E10: c₄ in c₁ ;
thus dom c₃ = dom c₂ by E8, E9, CARD_3:18
.= dom c₄ by E8, E10, CARD_3:18 ;

end;

registration

cluster non empty functional with_common_domain product-like set ;
existence

proof

consider c₁ being with_non-empty_elements set , c₂ being Function of 0,c₁;
take product c₂ ;
thus ( product c₂ is product-like & not product c₂ is empty ) ;

end;

theorem E8: :: AMISTD_2:7

for b₁ being functional with_common_domain set holds dom (PA b₁) = DOM b₁

proof

let c₁ be functional with_common_domain set ;

per cases not ( not c₁ is empty & c₁ is empty ) ;

suppose E9: c₁ is empty ;

hence dom (PA c₁) = {} by E6, RELAT_1:60
.= DOM c₁ by E9, PRALG_2:def 2 ;

end;

suppose E9: not c₁ is empty ;

consider c₂ being Element of c₁;

hereby :: uses TARSKI:def 3,XBOOLE_0:def 10

let c₃ be set ;
assume c₃ in dom (PA c₁) ;
then c₃ in dom c₂ by E9, E6;
hence c₃ in DOM c₁ by E9, PRALG_2:def 2;

end;let c₃ be set ; :: uses TARSKI:def 3
assume c₃ in DOM c₁ ;
then for b₁ being Function holds
( b₁ in c₁ implies c₃ in dom b₁ ) by PRALG_2:def 2;
hence c₃ in dom (PA c₁) by E9, E6;

end;

theorem :: AMISTD_2:8

for b₁ being functional set
for b₂ being set holds
( b₂ in dom (PA b₁) implies (PA b₁) . b₂ = pi b₁,b₂ )

proof

let c₁ be functional set ;
let c₂ be set ;

per cases not ( not c₁ = {} & not c₁ <> {} ) ;

suppose c₁ = {} ;

then dom (PA c₁) = dom {} by E6;
hence ( c₂ in dom (PA c₁) implies (PA c₁) . c₂ = pi c₁,c₂ ) ;

end;

suppose E9: c₁ <> {} ;

assume c₂ in dom (PA c₁) ;
hence (PA c₁) . c₂ = pi c₁,c₂ by E9, E6;

end;

theorem E9: :: AMISTD_2:9

for b₁ being functional with_common_domain set holds b₁ c= product (PA b₁)

proof

let c₁ be functional with_common_domain set ;
let c₂ be set ; :: uses TARSKI:def 3
assume E10: c₂ in c₁ ;
then reconsider c₃ = c₂ as Element of c₁ ;
E11: dom c₃ = DOM c₁ by E10, PRALG_2:def 2
.= dom (PA c₁) by E8 ;
for b₁ being set holds
( b₁ in dom (PA c₁) implies c₃ . b₁ in (PA c₁) . b₁ )

proof

let c₄ be set ;
assume c₄ in dom (PA c₁) ;
then (PA c₁) . c₄ = pi c₁,c₄ by E10, E6;
hence c₃ . c₄ in (PA c₁) . c₄ by E10, CARD_3:def 6;

end;

hence c₂ in product (PA c₁) by E11, CARD_3:18;

end;

theorem E10: :: AMISTD_2:10

for b₁ being non empty product-like set holds b₁ = product (PA b₁)

proof

let c₁ be non empty product-like set ;
thus c₁ c= product (PA c₁) by E9; :: uses XBOOLE_0:def 10
let c₂ be set ; :: uses TARSKI:def 3
assume c₂ in product (PA c₁) ;
then consider c₃ being Function such that
E11: c₂ = c₃
and E12: dom c₃ = dom (PA c₁)
and E13: for b₁ being set holds
( b₁ in dom (PA c₁) implies c₃ . b₁ in (PA c₁) . b₁ ) by CARD_3:def 5;
consider c₄ being Function such that
E14: c₁ = product c₄ by E7;
consider c₅ being Element of c₁;
E15: dom c₃ = DOM c₁ by E12, E8
.= dom c₅ by PRALG_2:def 2
.= dom c₄ by E14, CARD_3:18 ;
for b₁ being set holds
( b₁ in dom c₄ implies c₃ . b₁ in c₄ . b₁ )

proof

let c₆ be set ;
assume E16: c₆ in dom c₄ ;
then c₃ . c₆ in (PA c₁) . c₆ by E12, E13, E15;
then c₃ . c₆ in pi c₁,c₆ by E12, E15, E16, E6;
then ex b₁ being Function st
( b₁ in c₁ & c₃ . c₆ = b₁ . c₆ ) by CARD_3:def 6;
hence c₃ . c₆ in c₄ . c₆ by E14, E16, CARD_3:18;

end;

hence c₂ in c₁ by E11, E14, E15, CARD_3:18;

end;

registration

let c₁ be set ;
cluster -> functional FinSequenceSet of a₁;
coherence

proof

let c₂ be FinSequenceSet of c₁;
let c₃ be set ; :: uses FRAENKEL:def 1
thus ( c₃ in c₂ implies c₃ is Function ) by FINSEQ_2:def 3;

end;

registration

let c₁ be Nat;
let c₂ be set ;
cluster a₁ -tuples_on a₂ -> functional with_common_domain ;
coherence

proof

set c₃ = c₁ -tuples_on c₂;
let c₄, c₅ be Function; :: uses PRALG_2:def 1
assume E11: ( c₄ in c₁ -tuples_on c₂ & c₅ in c₁ -tuples_on c₂ ) ;
c₁ -tuples_on c₂ = { b₁ where B is Element of c₂ * : len b₁ = c₁ } by FINSEQ_2:def 4;
then ( ex b₁ being Element of c₂ * st
( c₄ = b₁ & len b₁ = c₁ ) & ex b₁ being Element of c₂ * st
( c₅ = b₁ & len b₁ = c₁ ) ) by E11;
hence dom c₄ = dom c₅ by FINSEQ_3:31;

end;

registration

let c₁ be Nat;
let c₂ be set ;
cluster a₁ -tuples_on a₂ -> functional with_common_domain product-like ;
coherence

proof

set c₃ = c₁ -tuples_on c₂;

per cases not ( not ( c₂ = {} & c₁ = 0 ) & not ( c₂ = {} & c₁ <> 0 ) & not c₂ <> {} ) ;

suppose ( c₂ = {} & c₁ = 0 ) ;

then c₁ -tuples_on c₂ = {(<*> c₂)} by FINSEQ_2:112
.= {{} } ;
hence c₁ -tuples_on c₂ is product-like by CARD_3:19;

end;

suppose ( c₂ = {} & c₁ <> 0 ) ;

then E11: c₁ -tuples_on c₂ = {} by CATALG_1:7;
take c₄ = 0 .--> {} ; :: uses AMISTD_2:def 2
rng c₄ = {{} } by CQC_LANG:5;
then {} in rng c₄ by TARSKI:def 1;
hence c₁ -tuples_on c₂ = product c₄ by E11, CARD_3:37;

end;

suppose c₂ <> {} ;

then reconsider c₄ = c₂ as non empty set ;
set c₅ = c₁ -tuples_on c₄;
take PA (c₁ -tuples_on c₄) ; :: uses AMISTD_2:def 2
c₁ -tuples_on c₄ = product (PA (c₁ -tuples_on c₄))

proof

thus c₁ -tuples_on c₄ c= product (PA (c₁ -tuples_on c₄)) by E9; :: uses XBOOLE_0:def 10
let c₆ be set ; :: uses TARSKI:def 3
assume c₆ in product (PA (c₁ -tuples_on c₄)) ;
then consider c₇ being Function such that
E11: c₆ = c₇
and E12: dom c₇ = dom (PA (c₁ -tuples_on c₄))
and E13: for b₁ being set holds
( b₁ in dom (PA (c₁ -tuples_on c₄)) implies c₇ . b₁ in (PA (c₁ -tuples_on c₄)) . b₁ ) by CARD_3:def 5;
E14: c₁ -tuples_on c₄ = { b₁ where B is Element of c₄ * : len b₁ = c₁ } by FINSEQ_2:def 4;
consider c₈ being Element of c₁ -tuples_on c₄;
c₈ in c₁ -tuples_on c₄ ;
then consider c₉ being Element of c₄ * such that
E15: c₈ = c₉
and E16: len c₉ = c₁ by E14;
E17: dom c₇ = DOM (c₁ -tuples_on c₄) by E12, E8
.= dom c₈ by PRALG_2:def 2 ;
dom c₈ = Seg (len c₉) by E15, FINSEQ_1:def 3;
then E18: c₇ is FinSequence by E17, FINSEQ_1:def 2;
rng c₇ c= c₄

proof

let c₁₀ be set ; :: uses TARSKI:def 3
assume c₁₀ in rng c₇ ;
then consider c₁₁ being set such that
E19: c₁₁ in dom c₇
and E20: c₇ . c₁₁ = c₁₀ by FUNCT_1:def 5;
c₇ . c₁₁ in (PA (c₁ -tuples_on c₄)) . c₁₁ by E12, E13, E19;
then c₇ . c₁₁ in pi (c₁ -tuples_on c₄),c₁₁ by E12, E19, E6;
then consider c₁₂ being Function such that
E21: c₁₂ in c₁ -tuples_on c₄
and E22: c₇ . c₁₁ = c₁₂ . c₁₁ by CARD_3:def 6;
consider c₁₃ being Element of c₄ * such that
E23: c₁₂ = c₁₃
and len c₁₃ = c₁ by E14, E21;
E24: rng c₁₃ c= c₄ by FINSEQ_1:def 4;
dom c₇ = dom c₁₃ by E17, E21, E23, PRALG_2:def 1;
then c₁₃ . c₁₁ in rng c₁₃ by E19, FUNCT_1:def 5;
hence c₁₀ in c₄ by E20, E22, E23, E24;

end;

then reconsider c₁₀ = c₇ as FinSequence of c₄ by E18, FINSEQ_1:def 4;
E19: c₁₀ in c₄ * by FINSEQ_1:def 11;
len c₁₀ = c₁ by E15, E16, E17, FINSEQ_3:31;
hence c₆ in c₁ -tuples_on c₄ by E11, E14, E19;

end;

hence c₁ -tuples_on c₂ = product (PA (c₁ -tuples_on c₄)) ;

end;

E11: for b₁ being natural number holds
- 1 < b₁

proof

let c₁ be natural number ;
( - 1 < 0 & 0 <= c₁ ) ;
hence - 1 < c₁ ;

end;

E12: for b₁ being natural number
for b₂, b₃, b₄ being Nat holds
not ( 1 <= b₂ & 2 <= b₃ & not b₁ < b₂ - 1 & not ( b₂ <= b₁ & b₁ <= (b₂ + b₃) - 3 ) & not b₁ = (b₂ + b₃) - 2 & not (b₂ + b₃) - 2 < b₁ & not b₁ = b₂ - 1 )

proof

let c₁ be natural number ;
let c₂, c₃, c₄ be Nat;
assume that E13: 1 <= c₂
and E14: 2 <= c₃
and E15: c₂ - 1 <= c₁
and E16: not ( not c₂ > c₁ & not c₁ > (c₂ + c₃) - 3 )
and E17: c₁ <> (c₂ + c₃) - 2
and E18: c₁ <= (c₂ + c₃) - 2 ;
E19: c₂ - 1 is Nat by E13, INT_1:18;

now

per cases not ( not c₁ < c₂ & not (c₂ + c₃) - 3 < c₁ ) by E16;

case c₁ < c₂ ;

then c₁ < (c₂ - 1) + 1 ;
hence c₁ <= c₂ - 1 by E19, NAT_1:38;

end;

case E20: (c₂ + c₃) - 3 < c₁ ;

1 + 2 <= c₂ + c₃ by E13, E14, XREAL_1:9;
then E21: (c₂ + c₃) - 3 is Nat by INT_1:18;
c₁ < ((c₂ + c₃) - 3) + 1 by E17, E18, REAL_1:def 5;
hence c₁ <= c₂ - 1 by E20, E21, NAT_1:38;

end;

hence c₂ - 1 = c₁ by E15, XREAL_1:1;

end;

theorem E13: :: AMISTD_2:11

for b₁, b₂ being set
for b₃ being AMI-Struct of b₂
for b₄ being FinPartState of b₃ holds
b₄ \ b₁ is FinPartState of b₃

proof

let c₁, c₂ be set ;
let c₃ be AMI-Struct of c₂;
let c₄ be FinPartState of c₃;
c₄ \ c₁ c= c₄ by XBOOLE_1:36;
then c₄ \ c₁ in sproduct the Object-Kind of c₃ by AMI_1:40;
hence c₄ \ c₁ is FinPartState of c₃ by AMI_1:def 24;

end;

theorem E14: :: AMISTD_2:12

for b₁ being set
for b₂ being with_non-empty_elements set
for b₃ being non empty non void IC-Ins-separated definite AMI-Struct of b₂
for b₄ being programmed FinPartState of b₃ holds
b₄ \ b₁ is programmed FinPartState of b₃

proof

let c₁ be set ;
let c₂ be with_non-empty_elements set ;
let c₃ be non empty non void IC-Ins-separated definite AMI-Struct of c₂;
let c₄ be programmed FinPartState of c₃;
reconsider c₅ = c₄ \ c₁ as FinPartState of c₃ by E13;

per cases not ( not c₅ is empty & c₅ is empty ) ;

suppose c₅ is empty ;

then reconsider c₆ = c₅ as empty FinPartState of c₃ ;
c₆ is programmed ;
hence c₄ \ c₁ is programmed FinPartState of c₃ ;

end;

suppose not c₅ is empty ;

then reconsider c₆ = c₅ as non empty FinPartState of c₃ ;
c₆ is programmed

proof

c₆ c= c₄ by XBOOLE_1:36;
then E15: dom c₆ c= dom c₄ by GRFUNC_1:8;
dom c₄ c= the Instruction-Locations of c₃ by AMI_3:def 13;
hence dom c₆ c= the Instruction-Locations of c₃ by E15, XBOOLE_1:1; :: uses AMI_3:def 13

end;

hence c₄ \ c₁ is programmed FinPartState of c₃ ;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃, c₄ be Instruction-Location of c₂;
let c₅, c₆ be Element of the Instructions of c₂;
redefine func --> as a₃,a₄ --> a₅,a₆ -> FinPartState of a₂;
coherence

proof

( ObjectKind c₃ = the Instructions of c₂ & ObjectKind c₄ = the Instructions of c₂ ) by AMI_1:def 14;
hence c₃,c₄ --> c₅,c₆ is FinPartState of c₂ by AMI_1:58;

end;

registration

let c₁ be with_non-empty_elements set ;
let c₂ be non void halting AMI-Struct of c₁;
cluster halting Element of the Instructions of a₂;
existence

proof

take halt c₂ ;
thus halt c₂ is halting ;

end;

theorem E15: :: AMISTD_2:13

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂
for b₄ being programmed FinPartState of b₂ holds
( dom b₃ = dom b₄ implies b₄ is lower )

proof

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be programmed lower FinPartState of c₂;
let c₄ be programmed FinPartState of c₂;
assume dom c₃ = dom c₄ ;
hence for b₁ being Instruction-Location of c₂ holds
( b₁ in dom c₄ implies for b₂ being Instruction-Location of c₂ holds
( b₂ <= b₁ implies b₂ in dom c₄ ) ) by AMISTD_1:def 20; :: uses AMISTD_1:def 20

end;

theorem E16: :: AMISTD_2:14

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂
for b₄ being Instruction-Location of b₂ holds
not ( b₄ in dom b₃ & not locnum b₄ < card b₃ )

proof

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite standard AMI-Struct of c₁;
let c₃ be programmed lower FinPartState of c₂;
let c₄ be Instruction-Location of c₂;
assume E17: c₄ in dom c₃ ;
c₄ = il. c₂,(locnum c₄) by AMISTD_1:def 13;
hence locnum c₄ < card c₃ by E17, AMISTD_1:50;

end;

theorem E17: :: AMISTD_2:15

for b₁ being with_non-empty_elements set
for b₂ being non empty non void IC-Ins-separated definite standard AMI-Struct of b₁
for b₃ being programmed lower FinPartState of b₂ holds dom b₃ = { (il. b₂,b₄) where B is Nat : b₄ < card b₃ }

proof

hereby :: uses TARSKI:def 3,XBOOLE_0:def 10

let c₄ be set ;
assume E19: c₄ in dom c₃ ;
then reconsider c₅ = c₄ as Instruction-Location of c₂ by E18;
E20: locnum c₅ < card c₃ by E19, E16;
reconsider c₆ = locnum c₅ as Element of NAT ;
c₅ = il. c₂,c₆ by AMISTD_1:def 13;
hence c₄ in { (il. c₂,b₁) where B is Nat : b₁ < card c₃ } by E20;

end; let c₄ be set ; :: uses TARSKI:def 3
assume c₄ in { (il. c₂,b₁) where B is Nat : b₁ < card c₃ } ;
then ex b₁ being Nat st
( c₄ = il. c₂,b₁ & b₁ < card c₃ ) ;
hence c₄ in dom c₃ by AMISTD_1:50;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
func AddressPart a₃ -> set equals :: AMISTD_2:def 3
a₃ `2 ;
coherence ;

end;

:: deftheorem defines AddressPart AMISTD_2:def 3 :

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be Element of the Instructions of c₂;
redefine func AddressPart as AddressPart a₃ -> FinSequence of (union a₁) \/ the carrier of a₂;
coherence

proof

AddressPart c₃ = c₃ `2 ;
hence AddressPart c₃ is FinSequence of (union c₁) \/ the carrier of c₂ by FINSEQ_1:def 11;

end;

theorem E18: :: AMISTD_2:16

for b₁ being set
for b₂ being AMI-Struct of b₁
for b₃, b₄ being Element of the Instructions of b₂ holds
( ( InsCode b₃ = InsCode b₄ & AddressPart b₃ = AddressPart b₄ ) implies ( b₃ = b₄ ) )

proof

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃, c₄ be Element of the Instructions of c₂;
assume E19: ( InsCode c₃ = InsCode c₄ & AddressPart c₃ = AddressPart c₄ ) ;
( ex b₁, b₂ being set st
( b₁ in the Instruction-Codes of c₂ & b₂ in ((union c₁) \/ the carrier of c₂) * & c₃ = [b₁,b₂] ) & ex b₁, b₂ being set st
( b₁ in the Instruction-Codes of c₂ & b₂ in ((union c₁) \/ the carrier of c₂) * & c₄ = [b₁,b₂] ) ) by ZFMISC_1:def 2;
then E20: ( c₃ = [(c₃ `1 ),(c₃ `2 )] & c₄ = [(c₄ `1 ),(c₄ `2 )] ) by MCART_1:8;
( InsCode c₃ = c₃ `1 & InsCode c₄ = c₄ `1 & AddressPart c₃ = c₃ `2 & AddressPart c₄ = c₄ `2 ) by AMI_5:def 1;
hence c₃ = c₄ by E19, E20;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
attr a₂ is homogeneous means :E19: :: AMISTD_2:def 4
for b₁, b₂ being Instruction of a₂ holds
( InsCode b₁ = InsCode b₂ implies dom (AddressPart b₁) = dom (AddressPart b₂) );

end;

:: deftheorem E19 defines homogeneous AMISTD_2:def 4 :

theorem E20: :: AMISTD_2:17

for b₁ being with_non-empty_elements set
for b₂ being Instruction of (STC b₁) holds AddressPart b₂ = 0

proof

let c₁ be with_non-empty_elements set ;
let c₂ be Instruction of (STC c₁);
the Instructions of (STC c₁) = {[0,0],[1,0]} by AMISTD_1:def 11;
then E21: ( c₂ = [0,0] or c₂ = [1,0] ) by TARSKI:def 2;
thus AddressPart c₂ = c₂ `2
.= 0 by E21, MCART_1:def 2 ;

end;

definition

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be InsType of c₂;
func AddressParts a₃ -> set equals :: AMISTD_2:def 5
{ (AddressPart b₁) where B is Instruction of a₂ : InsCode b₁ = a₃ } ;
coherence ;

end;

:: deftheorem defines AddressParts AMISTD_2:def 5 :

registration

let c₁ be set ;
let c₂ be AMI-Struct of c₁;
let c₃ be InsType of c₂;
cluster AddressParts a₃ -> functional ;
coherence

proof

let c₄ be set ; :: uses FRAENKEL:def 1
assume c₄ in AddressParts c₃ ;
then ex b₁ being Instruction of c₂ st
( c₄ = AddressPart b₁ & InsCode b₁ = c₃ ) ;
hence c₄ is Function ;

end;

definition

let c₁ be with_non-empty_elements set ;
let c₂ be non empty non void IC-Ins-separated definite AMI-Struct of c₁;
let c₃ be Instruction of c₂;
attr a₃ is with_explicit_jumps means :E21: :: AMISTD_2:def 6
for b₁ being set holds
not ( b₁ in JUMP a₃ & for b₂ being set holds
not ( b₂ in dom (AddressPart a₃) & b₁ = (AddressPart a₃) . b₂ & (PA (AddressParts (InsCode a₃))) . b₂ = the Instruction-Locations of a₂ ) );
attr a₃ is without_implicit_jumps means :E22: :: AMISTD_2:def 7
for b₁ being set holds
( ex b₂ being set st
( b₂ in dom (AddressPart a₃) & b₁ = (AddressPart a₃) . b₂ & (PA (AddressParts (InsCode a₃))) . b₂ = the Instruction-Locations of a₂ ) implies b₁ in JUMP a₃ );

end;

:: deftheorem E21 defines with_explicit_jumps AMISTD_2:def 6 :

:: deftheorem E22 defines without_implicit_jumps AMISTD_2:def 7 :