:: by Andrzej Trybulec

::

:: Received May 20, 2010

:: Copyright (c) 2010-2012 Association of Mizar Users

begin

:: deftheorem Def1 defines standard-ins COMPOS_0:def 1 :

for S being set holds

( S is standard-ins iff ex X being non empty set st S c= [:NAT,(NAT *),(X *):] );

for S being set holds

( S is standard-ins iff ex X being non empty set st S c= [:NAT,(NAT *),(X *):] );

registration
end;

notation

let x be set ;

synonym InsCode x for x `1_3 ;

synonym JumpPart x for x `2_3 ;

synonym AddressPart x for x `3_3 ;

end;
synonym InsCode x for x `1_3 ;

synonym JumpPart x for x `2_3 ;

synonym AddressPart x for x `3_3 ;

registration
end;

registration

let S be non empty standard-ins set ;

let I be Element of S;

coherence

( AddressPart I is Function-like & AddressPart I is Relation-like )

( JumpPart I is Function-like & JumpPart I is Relation-like )

end;
let I be Element of S;

coherence

( AddressPart I is Function-like & AddressPart I is Relation-like )

proof end;

coherence ( JumpPart I is Function-like & JumpPart I is Relation-like )

proof end;

registration

let S be non empty standard-ins set ;

let I be Element of S;

coherence

AddressPart I is FinSequence-like

JumpPart I is FinSequence-like

end;
let I be Element of S;

coherence

AddressPart I is FinSequence-like

proof end;

coherence JumpPart I is FinSequence-like

proof end;

registration

let S be non empty standard-ins set ;

let x be Element of S;

coherence

InsCode x is natural

end;
let x be Element of S;

coherence

InsCode x is natural

proof end;

registration
end;

:: deftheorem defines InsCodes COMPOS_0:def 2 :

for S being standard-ins set holds InsCodes S = proj1_3 S;

for S being standard-ins set holds InsCodes S = proj1_3 S;

registration
end;

definition

let S be non empty standard-ins set ;

let I be Element of S;

:: original: InsCode

redefine func InsCode I -> InsType of S;

coherence

InsCode I is InsType of S

end;
let I be Element of S;

:: original: InsCode

redefine func InsCode I -> InsType of S;

coherence

InsCode I is InsType of S

proof end;

definition

let S be non empty standard-ins set ;

let T be InsType of S;

{ (JumpPart I) where I is Element of S : InsCode I = T } is set ;

{ (AddressPart I) where I is Element of S : InsCode I = T } is set ;

end;
let T be InsType of S;

func JumpParts T -> set equals :: COMPOS_0:def 3

{ (JumpPart I) where I is Element of S : InsCode I = T } ;

coherence { (JumpPart I) where I is Element of S : InsCode I = T } ;

{ (JumpPart I) where I is Element of S : InsCode I = T } is set ;

func AddressParts T -> set equals :: COMPOS_0:def 4

{ (AddressPart I) where I is Element of S : InsCode I = T } ;

coherence { (AddressPart I) where I is Element of S : InsCode I = T } ;

{ (AddressPart I) where I is Element of S : InsCode I = T } is set ;

:: deftheorem defines JumpParts COMPOS_0:def 3 :

for S being non empty standard-ins set

for T being InsType of S holds JumpParts T = { (JumpPart I) where I is Element of S : InsCode I = T } ;

for S being non empty standard-ins set

for T being InsType of S holds JumpParts T = { (JumpPart I) where I is Element of S : InsCode I = T } ;

:: deftheorem defines AddressParts COMPOS_0:def 4 :

for S being non empty standard-ins set

for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Element of S : InsCode I = T } ;

for S being non empty standard-ins set

for T being InsType of S holds AddressParts T = { (AddressPart I) where I is Element of S : InsCode I = T } ;

registration

let S be non empty standard-ins set ;

let T be InsType of S;

coherence

AddressParts T is functional

( not JumpParts T is empty & JumpParts T is functional )

end;
let T be InsType of S;

coherence

AddressParts T is functional

proof end;

coherence ( not JumpParts T is empty & JumpParts T is functional )

proof end;

definition

let S be non empty standard-ins set ;

end;
attr S is homogeneous means :Def5: :: COMPOS_0:def 5

for I, J being Element of S st InsCode I = InsCode J holds

dom (JumpPart I) = dom (JumpPart J);

canceled;for I, J being Element of S st InsCode I = InsCode J holds

dom (JumpPart I) = dom (JumpPart J);

:: deftheorem Def5 defines homogeneous COMPOS_0:def 5 :

for S being non empty standard-ins set holds

( S is homogeneous iff for I, J being Element of S st InsCode I = InsCode J holds

dom (JumpPart I) = dom (JumpPart J) );

for S being non empty standard-ins set holds

( S is homogeneous iff for I, J being Element of S st InsCode I = InsCode J holds

dom (JumpPart I) = dom (JumpPart J) );

:: deftheorem Def7 defines J/A-independent COMPOS_0:def 7 :

for S being non empty standard-ins set holds

( S is J/A-independent iff for T being InsType of S

for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds

for p being set st [T,f1,p] in S holds

[T,f2,p] in S );

for S being non empty standard-ins set holds

( S is J/A-independent iff for T being InsType of S

for f1, f2 being natural-valued Function st f1 in JumpParts T & dom f1 = dom f2 holds

for p being set st [T,f1,p] in S holds

[T,f2,p] in S );

Lm1: for T being InsType of {[0,{},{}]} holds JumpParts T = {0}

proof end;

registration
end;

registration

existence

ex b_{1} being non empty standard-ins set st

( b_{1} is J/A-independent & b_{1} is homogeneous )

end;
ex b

( b

proof end;

registration

let S be non empty standard-ins homogeneous set ;

let T be InsType of S;

coherence

JumpParts T is with_common_domain

end;
let T be InsType of S;

coherence

JumpParts T is with_common_domain

proof end;

registration

let S be non empty standard-ins set ;

let I be Element of S;

coherence

for b_{1} being Function st b_{1} = JumpPart I holds

b_{1} is NAT -valued

end;
let I be Element of S;

coherence

for b

b

proof end;

Lm2: for S being non empty standard-ins homogeneous set

for I being Element of S

for x being set st x in dom (JumpPart I) holds

(product" (JumpParts (InsCode I))) . x c= NAT

proof end;

Lm3: for S being non empty standard-ins homogeneous set st S is J/A-independent holds

for I being Element of S

for x being set st x in dom (JumpPart I) holds

NAT c= (product" (JumpParts (InsCode I))) . x

proof end;

theorem Th1: :: COMPOS_0:1

for S being non empty standard-ins set

for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds

I = J

for I, J being Element of S st InsCode I = InsCode J & JumpPart I = JumpPart J & AddressPart I = AddressPart J holds

I = J

proof end;

registration

let S be non empty standard-ins homogeneous J/A-independent set ;

let T be InsType of S;

coherence

JumpParts T is product-like

end;
let T be InsType of S;

coherence

JumpParts T is product-like

proof end;

:: deftheorem Def8 defines ins-loc-free COMPOS_0:def 8 :

for S being standard-ins set

for I being Element of S holds

( I is ins-loc-free iff JumpPart I is empty );

for S being standard-ins set

for I being Element of S holds

( I is ins-loc-free iff JumpPart I is empty );

registration

let S be non empty standard-ins set ;

let I be Element of S;

coherence

for b_{1} being Function st b_{1} = JumpPart I holds

b_{1} is natural-valued
;

end;
let I be Element of S;

coherence

for b

b

definition

let S be non empty standard-ins homogeneous J/A-independent set ;

let I be Element of S;

let k be Nat;

ex b_{1} being Element of S st

( InsCode b_{1} = InsCode I & AddressPart b_{1} = AddressPart I & JumpPart b_{1} = k + (JumpPart I) )

for b_{1}, b_{2} being Element of S st InsCode b_{1} = InsCode I & AddressPart b_{1} = AddressPart I & JumpPart b_{1} = k + (JumpPart I) & InsCode b_{2} = InsCode I & AddressPart b_{2} = AddressPart I & JumpPart b_{2} = k + (JumpPart I) holds

b_{1} = b_{2}
by Th1;

end;
let I be Element of S;

let k be Nat;

func IncAddr (I,k) -> Element of S means :Def9: :: COMPOS_0:def 9

( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );

existence ( InsCode it = InsCode I & AddressPart it = AddressPart I & JumpPart it = k + (JumpPart I) );

ex b

( InsCode b

proof end;

uniqueness for b

b

:: deftheorem Def9 defines IncAddr COMPOS_0:def 9 :

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S

for k being Nat

for b_{4} being Element of S holds

( b_{4} = IncAddr (I,k) iff ( InsCode b_{4} = InsCode I & AddressPart b_{4} = AddressPart I & JumpPart b_{4} = k + (JumpPart I) ) );

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S

for k being Nat

for b

( b

theorem :: COMPOS_0:3

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds IncAddr (I,0) = I

for I being Element of S holds IncAddr (I,0) = I

proof end;

theorem Th4: :: COMPOS_0:4

for k being Nat

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S st I is ins-loc-free holds

IncAddr (I,k) = I

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S st I is ins-loc-free holds

IncAddr (I,k) = I

proof end;

theorem :: COMPOS_0:5

for k being Nat

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds JumpParts (InsCode I) = JumpParts (InsCode (IncAddr (I,k)))

proof end;

theorem Th6: :: COMPOS_0:6

for S being non empty standard-ins homogeneous J/A-independent set

for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds

I = J

for I, J being Element of S st ex k being Nat st IncAddr (I,k) = IncAddr (J,k) holds

I = J

proof end;

theorem :: COMPOS_0:7

for k, m being Nat

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S holds IncAddr ((IncAddr (I,k)),m) = IncAddr (I,(k + m))

proof end;

theorem :: COMPOS_0:8

for S being non empty standard-ins homogeneous J/A-independent set

for I being Element of S

for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

for I being Element of S

for x being set st x in dom (JumpPart I) holds

(JumpPart I) . x in (product" (JumpParts (InsCode I))) . x

proof end;

Lm4: for T being InsType of {[0,{},{}],[1,{},{}]} holds JumpParts T = {0}

proof end;

registration

coherence

( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )

end;
( {[0,{},{}],[1,{},{}]} is J/A-independent & {[0,{},{}],[1,{},{}]} is homogeneous )

proof end;

theorem :: COMPOS_0:10

for S being non empty standard-ins set

for T being InsType of S ex I being Element of S st InsCode I = T

for T being InsType of S ex I being Element of S st InsCode I = T

proof end;

theorem :: COMPOS_0:11

for S being non empty standard-ins homogeneous set

for I being Element of S st JumpPart I = {} holds

JumpParts (InsCode I) = {0}

for I being Element of S st JumpPart I = {} holds

JumpParts (InsCode I) = {0}

proof end;

begin

:: deftheorem Def10 defines with_halt COMPOS_0:def 10 :

for X being set holds

( X is with_halt iff [0,{},{}] in X );

for X being set holds

( X is with_halt iff [0,{},{}] in X );

registration
end;

registration

coherence

{[0,{},{}]} is with_halt

{[0,{},{}],[1,{},{}]} is with_halt

end;
{[0,{},{}]} is with_halt

proof end;

coherence {[0,{},{}],[1,{},{}]} is with_halt

proof end;

registration
end;

registration

existence

ex b_{1} being standard-ins with_halt set st

( b_{1} is J/A-independent & b_{1} is homogeneous )

end;
ex b

( b

proof end;

registration

let S be standard-ins with_halt set ;

existence

ex b_{1} being Element of S st b_{1} is ins-loc-free

end;
existence

ex b

proof end;

registration

let S be standard-ins with_halt set ;

let I be ins-loc-free Element of S;

coherence

JumpPart I is empty by Def8;

end;
let I be ins-loc-free Element of S;

coherence

JumpPart I is empty by Def8;

theorem :: COMPOS_0:12

for k being Nat

for S being non empty standard-ins homogeneous J/A-independent with_halt set

for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

for S being non empty standard-ins homogeneous J/A-independent with_halt set

for I being Element of S st IncAddr (I,k) = halt S holds

I = halt S

proof end;

definition
end;

:: deftheorem defines No-StopCode COMPOS_0:def 12 :

for S being non empty standard-ins homogeneous J/A-independent with_halt set

for i being Element of S holds

( i is No-StopCode iff i <> halt S );

for S being non empty standard-ins homogeneous J/A-independent with_halt set

for i being Element of S holds

( i is No-StopCode iff i <> halt S );

begin

registration

not for b_{1} being Instructions holds b_{1} is trivial
end;

cluster non empty non trivial Relation-like standard-ins homogeneous J/A-independent with_halt for set ;

existence not for b

proof end;

:: zero i zeby ta instrukcja to byla [0,{},{}], a wiec ma byc jedyna

:: instrukcja o kodzie 0. Wymaga to modyfikacji

:: maszyny SCMPDS, gdzie z instrukcje halt robi goto 0 (tzn. przeskok

:: o 0);