:: Input and Output of Instructions
:: by Artur Korni{\l}owicz
::
:: Copyright (c) 2001-2019 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 ;
coherence
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b1 is with_explicit_jumps & b1 is IC-relocable & b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions )
proof end;
end;

registration
let N be with_zero set ;
coherence
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is with_non_trivial_ObjectKinds & b1 is with_non_trivial_Instructions & b1 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 () -> non trivial ;
coherence
not Values () 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 b1 being Subset of A st
for o being Object of A holds
( o in b1 iff ex s being State of A st s . o <> (Exec (I,s)) . o )
proof end;
uniqueness
for b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) & ( for o being Object of A holds
( o in b2 iff ex s being State of A st s . o <> (Exec (I,s)) . o ) ) holds
b1 = b2
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 b4 being Subset of A holds
( b4 = Output I iff for o being Object of A holds
( o in b4 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 b1 being Subset of A st
for o being Object of A holds
( o in b1 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 b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 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 b2 iff for s being State of A
for a being Element of Values o holds Exec (I,s) = Exec (I,(s +* (o,a))) ) ) holds
b1 = b2
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 b1 being Subset of A st
for o being Object of A holds
( o in b1 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 b1, b2 being Subset of A st ( for o being Object of A holds
( o in b1 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 b2 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
b1 = b2
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 b4 being Subset of A holds
( b4 = Out_\_Inp I iff for o being Object of A holds
( o in b4 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 b4 being Subset of A holds
( b4 = Out_U_Inp I iff for o being Object of A holds
( o in b4 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
() \ ();
coherence
() \ () 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 = () \ ();

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 = () \ ()
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 = () \/ ()
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;
coherence
Input I is empty
by Th13;
coherence
Output I is empty
by Th10;
coherence by Th12;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is halting & b1 is with_non_trivial_ObjectKinds & b1 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;
coherence by Th11;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values AMI-Struct over N st
( b1 is with_non_trivial_Instructions & b1 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 s holds
IC in Output I by Def3;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N st b1 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 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;