:: Input and Output of Instructions
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001 Association of Mizar Users

begin

theorem :: AMI_7:1

canceled;

theorem Th2: :: AMI_7:2

for N being non empty with_non-empty_elements set
for A being non empty stored-program AMI-Struct of N
for s being State of A
for o being Object of A holds s . o in ObjectKind o

proof end;

theorem :: AMI_7:3

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite realistic AMI-Struct of N
for s being State of A
for f being Element of NAT
for w being Element of ObjectKind (IC A) holds (s +* (IC A),w) . f = s . f by AMI_1:48, FUNCT_7:34;

definition

let N be non empty with_non-empty_elements set ;
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let s be State of A;
let o be Object of A;
let a be Element of ObjectKind o;
:: original: +*
redefine func s +* o,a -> State of A;
coherence
s +* o,a is State of A

proof end;

end;

theorem :: AMI_7:4

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated steady-programmed definite AMI-Struct of N
for s being State of A
for o being Object of A
for f being Element of NAT
for I being Instruction of A
for w being Element of ObjectKind o st f <> o holds
(Exec I,s) . f = (Exec I,(s +* o,w)) . f

proof end;

theorem :: AMI_7:5

canceled;

theorem Th6: :: AMI_7:6

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,s) = IC (Exec I,(s +* o,w))

proof end;

theorem :: AMI_7:7

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o st I is sequential & o <> IC A holds
IC (Exec I,(s +* o,w)) = IC ((Exec I,s) +* o,w)

proof end;

theorem :: AMI_7:8

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated steady-programmed definite standard AMI-Struct of N
for I being Instruction of A
for s being State of A
for o being Object of A
for w being Element of ObjectKind o
for i being Element of NAT holds (Exec I,(s +* o,w)) . i = ((Exec I,s) +* o,w) . i

proof end;

begin

definition

let N be set ;
let A be AMI-Struct of N;
attr A is with_non_trivial_Instructions means :Def1: :: AMI_7:def 1
not the Instructions of A is trivial ;

end;

:: deftheorem Def1 defines with_non_trivial_Instructions AMI_7:def 1 :

for N being set
for A being AMI-Struct of N holds
( A is with_non_trivial_Instructions iff not the Instructions of A is trivial );

definition

let N be set ;
let A be non empty AMI-Struct of N;
attr A is with_non_trivial_ObjectKinds means :Def2: :: AMI_7:def 2
for o being Object of A holds not ObjectKind o is trivial ;

end;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMI_7:def 2 :

for N being set
for A being non empty AMI-Struct of N holds
( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not ObjectKind o is trivial );

registration

let N be with_non-empty_elements set ;
cluster STC N -> with_non_trivial_ObjectKinds ;
coherence
STC N is with_non_trivial_ObjectKinds

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program halting IC-Ins-separated steady-programmed definite realistic standard-ins InsLoc-antisymmetric standard V83(N) with_explicit_jumps without_implicit_jumps regular IC-good Exec-preserving with_non_trivial_Instructions with_non_trivial_ObjectKinds AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite standard-ins standard regular AMI-Struct of N st
( b₁ is halting & b₁ is realistic & b₁ is steady-programmed & b₁ is with_explicit_jumps & b₁ is without_implicit_jumps & b₁ is IC-good & b₁ is Exec-preserving & b₁ is with_non_trivial_ObjectKinds & b₁ is with_non_trivial_Instructions )

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster non empty stored-program definite with_non_trivial_ObjectKinds -> non empty stored-program definite with_non_trivial_Instructions AMI-Struct of N;
coherence
for b₁ being non empty stored-program definite AMI-Struct of N st b₁ is with_non_trivial_ObjectKinds holds
b₁ is with_non_trivial_Instructions

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite with_non_trivial_Instructions with_non_trivial_ObjectKinds AMI-Struct of N;
existence
ex b₁ being non empty stored-program AMI-Struct of N st
( b₁ is with_non_trivial_ObjectKinds & b₁ is with_non_trivial_Instructions & b₁ is IC-Ins-separated & b₁ is definite )

proof end;

end;

registration

let N be with_non-empty_elements set ;
let A be non empty with_non_trivial_ObjectKinds AMI-Struct of N;
let o be Object of A;
cluster ObjectKind o -> non trivial ;
coherence
not ObjectKind o is trivial by Def2;

end;

registration

let N be with_non-empty_elements set ;
let A be with_non_trivial_Instructions AMI-Struct of N;
cluster the Instructions of A -> non trivial ;
coherence
not the Instructions of A is trivial by Def1;

end;

registration

let N be with_non-empty_elements set ;
let A be non empty IC-Ins-separated AMI-Struct of N;
cluster ObjectKind (IC A) -> non trivial ;
coherence
not ObjectKind (IC A) is trivial by AMI_1:def 11;

end;

definition

let N be with_non-empty_elements set ;
let A be non empty stored-program AMI-Struct of N;
let I be Instruction of A;
func Output I -> Subset of A means :Def3: :: AMI_7:def 3
for o being Object of A holds
( o in it iff ex s being State of A st s . o <> (Exec I,s) . o );
existence
ex b₁ being Subset of A st
for o being Object of A holds
( o in b₁ iff ex s being State of A st s . o <> (Exec I,s) . o )

proof end;

uniqueness
for b₁, b₂ being Subset of A st ( for o being Object of A holds
( o in b₁ iff ex s being State of A st s . o <> (Exec I,s) . o ) ) & ( for o being Object of A holds
( o in b₂ iff ex s being State of A st s . o <> (Exec I,s) . o ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def3 defines Output AMI_7:def 3 :

for N being with_non-empty_elements set
for A being non empty stored-program AMI-Struct of N
for I being Instruction of A
for b₄ being Subset of A holds
( b₄ = Output I iff for o being Object of A holds
( o in b₄ iff ex s being State of A st s . o <> (Exec I,s) . o ) );

definition

let N be non empty with_non-empty_elements set ;
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let I be Instruction of A;
func Out_\_Inp I -> Subset of A means :Def4: :: AMI_7:def 4
for o being Object of A holds
( o in it iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) );
existence
ex b₁ being Subset of A st
for o being Object of A holds
( o in b₁ iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) )

proof end;

uniqueness
for b₁, b₂ being Subset of A st ( for o being Object of A holds
( o in b₁ iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) & ( for o being Object of A holds
( o in b₂ iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) ) holds
b₁ = b₂

proof end;

func Out_U_Inp I -> Subset of A means :Def5: :: AMI_7:def 5
for o being Object of A holds
( o in it iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a );
existence
ex b₁ being Subset of A st
for o being Object of A holds
( o in b₁ iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a )

proof end;

uniqueness
for b₁, b₂ being Subset of A st ( for o being Object of A holds
( o in b₁ iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) & ( for o being Object of A holds
( o in b₂ iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Out_\_Inp AMI_7:def 4 :

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for b₄ being Subset of A holds
( b₄ = Out_\_Inp I iff for o being Object of A holds
( o in b₄ iff for s being State of A
for a being Element of ObjectKind o holds Exec I,s = Exec I,(s +* o,a) ) );

:: deftheorem Def5 defines Out_U_Inp AMI_7:def 5 :

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for b₄ being Subset of A holds
( b₄ = Out_U_Inp I iff for o being Object of A holds
( o in b₄ iff ex s being State of A ex a being Element of ObjectKind o st Exec I,(s +* o,a) <> (Exec I,s) +* o,a ) );

definition

let N be non empty with_non-empty_elements set ;
let A be non empty stored-program IC-Ins-separated definite AMI-Struct of N;
let I be Instruction of A;
func Input I -> Subset of A equals :: AMI_7:def 6
(Out_U_Inp I) \ (Out_\_Inp I);
coherence
(Out_U_Inp I) \ (Out_\_Inp I) is Subset of A ;

end;

:: deftheorem defines Input AMI_7:def 6 :

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);

theorem :: AMI_7:9

canceled;

theorem Th10: :: AMI_7:10

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_\_Inp I c= Output I

proof end;

theorem Th11: :: AMI_7:11

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds Output I c= Out_U_Inp I

proof end;

theorem :: AMI_7:12

canceled;

theorem :: AMI_7:13

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)

proof end;

theorem :: AMI_7:14

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)

proof end;

theorem Th15: :: AMI_7:15

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Out_U_Inp I

proof end;

theorem :: AMI_7:16

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Input I

proof end;

theorem :: AMI_7:17

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Output I

proof end;

theorem Th18: :: AMI_7:18

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A holds
( I is halting iff Output I is empty )

proof end;

theorem Th19: :: AMI_7:19

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_\_Inp I is empty

proof end;

theorem Th20: :: AMI_7:20

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Out_U_Inp I is empty

proof end;

theorem Th21: :: AMI_7:21

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st I is halting holds
Input I is empty

proof end;

registration

let N be non empty with_non-empty_elements set ;
let A be non empty stored-program halting IC-Ins-separated definite AMI-Struct of N;
let I be halting Instruction of A;
cluster Input I -> empty ;
coherence
Input I is empty by Th21;
cluster Output I -> empty ;
coherence
Output I is empty by Th18;
cluster Out_U_Inp I -> empty ;
coherence
Out_U_Inp I is empty by Th20;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program halting IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N;
existence
ex b₁ being non empty stored-program AMI-Struct of N st
( b₁ is halting & b₁ is with_non_trivial_ObjectKinds & b₁ is IC-Ins-separated & b₁ is definite )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let A be non empty stored-program halting IC-Ins-separated definite with_non_trivial_ObjectKinds AMI-Struct of N;
let I be halting Instruction of A;
cluster Out_\_Inp I -> empty ;
coherence
Out_\_Inp I is empty by Th19;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of N;
existence
ex b₁ being non empty stored-program AMI-Struct of N st
( b₁ is with_non_trivial_Instructions & b₁ is steady-programmed & b₁ is IC-Ins-separated & b₁ is definite )

proof end;

end;

theorem :: AMI_7:22

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated steady-programmed definite with_non_trivial_Instructions AMI-Struct of N
for f being Element of NAT
for I being Instruction of A holds not f in Out_\_Inp I

proof end;

theorem :: AMI_7:23

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
not IC A in Out_\_Inp I

proof end;

theorem :: AMI_7:24

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st ex s being State of A st (Exec I,s) . (IC A) <> IC s holds
IC A in Output I by Def3;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite standard AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite AMI-Struct of N st b₁ is standard

proof end;

end;

theorem :: AMI_7:25

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
IC A in Output I

proof end;

theorem Th26: :: AMI_7:26

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for I being Instruction of A st ex s being State of A st (Exec I,s) . (IC A) <> IC s holds
IC A in Out_U_Inp I

proof end;

theorem :: AMI_7:27

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard AMI-Struct of N
for I being Instruction of A st I is sequential holds
IC A in Out_U_Inp I

proof end;

theorem :: AMI_7:28

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of N
for f being Element of NAT
for I being Instruction of A st ( for s being State of A
for p being NAT -defined FinPartState of holds Exec I,(s +* p) = (Exec I,s) +* p ) holds
not f in Out_U_Inp I

proof end;

theorem :: AMI_7:29

for N being non empty with_non-empty_elements set
for A being non empty stored-program IC-Ins-separated definite standard-ins AMI-Struct of N
for I being Instruction of A
for o being Object of A st I is jump-only & o in Output I holds
o = IC A

proof end;