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

begin

definition

let N be non empty with_non-empty_elements set ;
let A be non empty IC-Ins-separated 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 Th6: :: AMISTD_4:1

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 holds
IC (Exec (I,s)) = IC (Exec (I,(s +* (o,w))))

proof end;

theorem :: AMISTD_4:2

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 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: :: AMISTD_4:def 1
not the Instructions of A is trivial ;

end;

:: deftheorem Def1 defines with_non_trivial_Instructions AMISTD_4: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: :: AMISTD_4:def 2
for o being Object of A holds not ObjectKind o is trivial ;

end;

:: deftheorem Def2 defines with_non_trivial_ObjectKinds AMISTD_4: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 standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting with_explicit_jumps IC-relocable standard with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct of N;
existence
ex b₁ being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting standard AMI-Struct of 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_non-empty_elements set ;
cluster STC N -> with_non_trivial_Instructions ;
coherence
STC N is with_non_trivial_Instructions

proof end;

end;

registration

let N be with_non-empty_elements set ;
cluster non empty IC-Ins-separated with_non_trivial_Instructions with_non_trivial_ObjectKinds for AMI-Struct of N;
existence
ex b₁ being non empty AMI-Struct of 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_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 ) -> non trivial ;
coherence
not ObjectKind (IC ) is trivial by MEMSTR_0:def 3;

end;

definition

let N be with_non-empty_elements set ;
let A be non empty AMI-Struct of 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_non-empty_elements set
for A being non empty 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 IC-Ins-separated AMI-Struct of 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 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: :: 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 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 AMISTD_4:def 4 :
for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 AMISTD_4:def 5 :
for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 IC-Ins-separated AMI-Struct of 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 non empty with_non-empty_elements set
for A being non empty IC-Ins-separated AMI-Struct of N
for I being Instruction of A holds Input I = (Out_U_Inp I) \ (Out_\_Inp I);

theorem Th10: :: AMISTD_4:3

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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: :: AMISTD_4:4

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

proof end;

theorem :: AMISTD_4:5

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 :: AMISTD_4:6

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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: :: AMISTD_4:7

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 :: AMISTD_4:8

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 :: AMISTD_4:9

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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: :: AMISTD_4:10

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

proof end;

theorem Th19: :: AMISTD_4:11

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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: :: AMISTD_4:12

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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: :: AMISTD_4:13

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated 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 IC-Ins-separated 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 IC-Ins-separated halting with_non_trivial_ObjectKinds for AMI-Struct of N;
existence
ex b₁ being non empty AMI-Struct of N st
( b₁ is halting & b₁ is with_non_trivial_ObjectKinds & b₁ is IC-Ins-separated )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let A be non empty IC-Ins-separated 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 IC-Ins-separated with_non_trivial_Instructions for AMI-Struct of N;
existence
ex b₁ being non empty AMI-Struct of N st
( b₁ is with_non_trivial_Instructions & b₁ is IC-Ins-separated )

proof end;

end;

theorem :: AMISTD_4:14

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated standard AMI-Struct of 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 non empty with_non-empty_elements set
for A being non empty IC-Ins-separated AMI-Struct of 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 non empty with_non-empty_elements set ;
cluster non empty IC-Ins-separated standard for AMI-Struct of N;
existence
ex b₁ being non empty IC-Ins-separated AMI-Struct of N st b₁ is standard

proof end;

end;

theorem :: AMISTD_4:16

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

proof end;

theorem Th26: :: AMISTD_4:17

for N being non empty with_non-empty_elements set
for A being non empty IC-Ins-separated AMI-Struct of 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 non empty with_non-empty_elements set
for A being non empty IC-Ins-separated standard AMI-Struct of 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 non empty with_non-empty_elements set
for A being standard-ins non empty IC-Ins-separated 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

proof end;