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

definition

let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let s be State of A;
let o be Object of A;
let a be Element of Values o;
:: original: +*
redefine func s +* (o,a) -> State of A;
coherence
s +* (o,a) is State of A

proof end;

end;

theorem Th1: :: AMISTD_4:1

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

proof end;

theorem :: AMISTD_4:2

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

proof end;

definition

let A be COM-Struct ;

attr A is with_non_trivial_Instructions means :Def1: :: AMISTD_4:def 1
not the InstructionsF of A is trivial ;

end;

:: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4:def 1 :
for A being COM-Struct holds
( A is with_non_trivial_Instructions iff not the InstructionsF of A is trivial );

definition

let N be with_zero set ;
let A be non empty with_non-empty_values AMI-Struct over N;

attr A is with_non_trivial_ObjectKinds means :Def2: :: AMISTD_4:def 2
for o being Object of A holds not Values o is trivial ;

end;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4:def 2 :
for N being with_zero set
for A being non empty with_non-empty_values AMI-Struct over N holds
( A is with_non_trivial_ObjectKinds iff for o being Object of A holds not Values o is trivial );

registration

let N be with_zero set ;

cluster STC N -> with_non_trivial_ObjectKinds ;

coherence
STC N is with_non_trivial_ObjectKinds

proof end;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps IC-relocable standard with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b₁ is with_explicit_jumps & b₁ is IC-relocable & b₁ is with_non_trivial_ObjectKinds & b₁ is with_non_trivial_Instructions )

proof end;

end;

registration

let N be with_zero set ;

cluster STC N -> with_non_trivial_Instructions ;

coherence
STC N is with_non_trivial_Instructions

proof end;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values AMI-Struct over N st
( b₁ is with_non_trivial_ObjectKinds & b₁ is with_non_trivial_Instructions & b₁ is IC-Ins-separated )

proof end;

end;

registration

let N be with_zero set ;
let A be non empty with_non-empty_values with_non_trivial_ObjectKinds AMI-Struct over N;
let o be Object of A;

cluster Values o -> non trivial ;

coherence
not Values o is trivial by Def2;

end;

registration

let N be with_zero set ;
let A be with_non-empty_values with_non_trivial_Instructions AMI-Struct over N;

cluster the InstructionsF of A -> non trivial ;

coherence
not the InstructionsF of A is trivial by Def1;

end;

registration

let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;

cluster Values (IC ) -> non trivial ;

coherence
not Values (IC ) is trivial by MEMSTR_0:def 6;

end;

definition

let N be with_zero set ;
let A be non empty with_non-empty_values AMI-Struct over N;
let I be Instruction of A;

func Output I -> Subset of A means :Def3: :: AMISTD_4: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 AMISTD_4:def 3 :
for N being with_zero set
for A being non empty with_non-empty_values AMI-Struct over 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 with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let I be Instruction of A;

func Out_\_Inp I -> Subset of A means :Def4: :: AMISTD_4:def 4
for o being Object of A holds
( o in it iff for s being State of A
for a being Element of Values 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 Values 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 Values 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 Values 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: :: AMISTD_4:def 5
for o being Object of A holds
( o in it iff ex s being State of A ex a being Element of Values 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 Values 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 Values 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 Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def4 defines Out_\_Inp AMISTD_4:def 4 :
for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) );

:: deftheorem Def5 defines Out_U_Inp AMISTD_4:def 5 :
for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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 Values o st Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) ) );

definition

let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N;
let I be Instruction of A;

func Input I -> Subset of A equals :: AMISTD_4: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 AMISTD_4:def 6 :
for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);

theorem Th3: :: AMISTD_4:3

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A holds Out_\_Inp I c= Output I

proof end;

theorem Th4: :: AMISTD_4:4

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A holds Output I c= Out_U_Inp I

proof end;

theorem :: AMISTD_4:5

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A holds Out_\_Inp I = (Output I) \ (Input I)

proof end;

theorem :: AMISTD_4:6

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A holds Out_U_Inp I = (Output I) \/ (Input I)

proof end;

theorem Th7: :: AMISTD_4:7

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Out_U_Inp I

proof end;

theorem :: AMISTD_4:8

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Input I

proof end;

theorem :: AMISTD_4:9

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A
for o being Object of A st Values o is trivial holds
not o in Output I

proof end;

theorem Th10: :: AMISTD_4:10

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A holds
( I is halting iff Output I is empty )

proof end;

theorem Th11: :: AMISTD_4:11

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated with_non_trivial_ObjectKinds AMI-Struct over N
for I being Instruction of A st I is halting holds
Out_\_Inp I is empty

proof end;

theorem Th12: :: AMISTD_4:12

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A st I is halting holds
Out_U_Inp I is empty

proof end;

theorem Th13: :: AMISTD_4:13

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of A st I is halting holds
Input I is empty

proof end;

registration

let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let I be halting Instruction of A;

cluster Input I -> empty ;

coherence
Input I is empty by Th13;

cluster Output I -> empty ;

coherence
Output I is empty by Th10;

cluster Out_U_Inp I -> empty ;

coherence
Out_U_Inp I is empty by Th12;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values AMI-Struct over N st
( b₁ is halting & b₁ is with_non_trivial_ObjectKinds & b₁ is IC-Ins-separated )

proof end;

end;

registration

let N be with_zero set ;
let A be non empty with_non-empty_values IC-Ins-separated halting with_non_trivial_ObjectKinds AMI-Struct over N;
let I be halting Instruction of A;

cluster Out_\_Inp I -> empty ;

coherence
Out_\_Inp I is empty by Th11;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated with_non_trivial_Instructions for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values AMI-Struct over N st
( b₁ is with_non_trivial_Instructions & b₁ is IC-Ins-separated )

proof end;

end;

theorem :: AMISTD_4:14

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of A st I is sequential holds
not IC in Out_\_Inp I

proof end;

theorem :: AMISTD_4:15

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

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated standard for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b₁ is standard

proof end;

end;

theorem :: AMISTD_4:16

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of A st I is sequential holds
IC in Output I

proof end;

theorem Th17: :: AMISTD_4:17

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

proof end;

theorem :: AMISTD_4:18

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N
for I being Instruction of A st I is sequential holds
IC in Out_U_Inp I

proof end;

theorem :: AMISTD_4:19

for N being with_zero set
for A being non empty with_non-empty_values IC-Ins-separated AMI-Struct over 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

proof end;