:: by Artur Korni{\l}owicz

::

:: Received December 10, 2003

:: Copyright (c) 2003-2021 Association of Mizar Users

:: LocSeq

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be Subset of NAT;

deffunc H_{1}( object ) -> set = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . $1;

ex b_{1} being Sequence of NAT st

( dom b_{1} = card M & ( for m being set st m in card M holds

b_{1} . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) )

for b_{1}, b_{2} being Sequence of NAT st dom b_{1} = card M & ( for m being set st m in card M holds

b_{1} . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) & dom b_{2} = card M & ( for m being set st m in card M holds

b_{2} . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) holds

b_{1} = b_{2}

end;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be Subset of NAT;

deffunc H

func LocSeq (M,S) -> Sequence of NAT means :Def1: :: AMISTD_3:def 1

( dom it = card M & ( for m being set st m in card M holds

it . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) );

existence ( dom it = card M & ( for m being set st m in card M holds

it . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines LocSeq AMISTD_3:def 1 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for M being Subset of NAT

for b_{4} being Sequence of NAT holds

( b_{4} = LocSeq (M,S) iff ( dom b_{4} = card M & ( for m being set st m in card M holds

b_{4} . m = (canonical_isomorphism_of ((RelIncl (order_type_of (RelIncl M))),(RelIncl M))) . m ) ) );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for M being Subset of NAT

for b

( b

b

theorem :: AMISTD_3:1

for n being Nat

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for F being Subset of NAT st F = {n} holds

LocSeq (F,S) = 0 .--> n

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for F being Subset of NAT st F = {n} holds

LocSeq (F,S) = 0 .--> n

proof end;

registration

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be Subset of NAT;

coherence

LocSeq (M,S) is one-to-one

end;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be Subset of NAT;

coherence

LocSeq (M,S) is one-to-one

proof end;

:: Tree of Execution

definition

let N be with_zero set ;

let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be non empty preProgram of S;

ex b_{1} being DecoratedTree of NAT st

( b_{1} . {} = FirstLoc M & ( for t being Element of dom b_{1} holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b_{1} . t)),(b_{1} . t))) } & ( for m being Nat st m in card (NIC ((M /. (b_{1} . t)),(b_{1} . t))) holds

b_{1} . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b_{1} . t)),(b_{1} . t))),S)) . m ) ) ) )

for b_{1}, b_{2} being DecoratedTree of NAT st b_{1} . {} = FirstLoc M & ( for t being Element of dom b_{1} holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b_{1} . t)),(b_{1} . t))) } & ( for m being Nat st m in card (NIC ((M /. (b_{1} . t)),(b_{1} . t))) holds

b_{1} . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b_{1} . t)),(b_{1} . t))),S)) . m ) ) ) & b_{2} . {} = FirstLoc M & ( for t being Element of dom b_{2} holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b_{2} . t)),(b_{2} . t))) } & ( for m being Nat st m in card (NIC ((M /. (b_{2} . t)),(b_{2} . t))) holds

b_{2} . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b_{2} . t)),(b_{2} . t))),S)) . m ) ) ) holds

b_{1} = b_{2}

end;
let S be non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N;

let M be non empty preProgram of S;

func ExecTree M -> DecoratedTree of NAT means :Def2: :: AMISTD_3:def 2

( it . {} = FirstLoc M & ( for t being Element of dom it holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (it . t)),(it . t))) } & ( for m being Nat st m in card (NIC ((M /. (it . t)),(it . t))) holds

it . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (it . t)),(it . t))),S)) . m ) ) ) );

existence ( it . {} = FirstLoc M & ( for t being Element of dom it holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (it . t)),(it . t))) } & ( for m being Nat st m in card (NIC ((M /. (it . t)),(it . t))) holds

it . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (it . t)),(it . t))),S)) . m ) ) ) );

ex b

( b

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b

b

proof end;

uniqueness for b

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b

b

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b

b

b

proof end;

:: deftheorem Def2 defines ExecTree AMISTD_3:def 2 :

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for M being non empty preProgram of S

for b_{4} being DecoratedTree of NAT holds

( b_{4} = ExecTree M iff ( b_{4} . {} = FirstLoc M & ( for t being Element of dom b_{4} holds

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b_{4} . t)),(b_{4} . t))) } & ( for m being Nat st m in card (NIC ((M /. (b_{4} . t)),(b_{4} . t))) holds

b_{4} . (t ^ <*m*>) = (LocSeq ((NIC ((M /. (b_{4} . t)),(b_{4} . t))),S)) . m ) ) ) ) );

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated standard AMI-Struct over N

for M being non empty preProgram of S

for b

( b

( succ t = { (t ^ <*k*>) where k is Nat : k in card (NIC ((M /. (b

b

theorem :: AMISTD_3:2

for N being with_zero set

for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0

for S being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N holds ExecTree (Stop S) = TrivialInfiniteTree --> 0

proof end;