:: 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 COMPOS_1:3, 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

canceled;

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;

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 IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting standard with_explicit_jumps 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 realistic standard-ins homogeneous regular J/A-independent halting standard AMI-Struct of N st
( b₁ is with_explicit_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 COMPOS_1:def 6;

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:8

canceled;

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 IC-Ins-separated definite halting 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 IC-Ins-separated definite halting 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 IC-Ins-separated definite halting 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 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 IC-Ins-separated & b₁ is definite )

proof end;

end;

theorem :: AMI_7:22

canceled;

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;