begin
begin
Lm1:
for k being Element of NAT
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N holds k <= k,S
set III = {[1,0,0],[0,0,0]};
begin
Lm2:
for N being with_zero set
for i being Instruction of (STC N)
for s being State of (STC N) st InsCode i = 1 holds
IC (Exec (i,s)) = succ (IC s)
Lm3:
for z being Nat
for N being with_zero set
for l being Element of NAT
for i being Element of the InstructionsF of (STC N) st l = z & InsCode i = 1 holds
NIC (i,l) = {(z + 1)}
definition
let N be
with_zero set ;
let S be non
empty with_non-empty_values IC-Ins-separated weakly_standard AMI-Struct over
N;
let k be
Nat;
existence
ex b1 being Element of NAT ex f being Function of NAT,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b1 = f . k )
uniqueness
for b1, b2 being Element of NAT st ex f being Function of NAT,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b1 = f . k ) & ex f being Function of NAT,NAT st
( f is bijective & ( for m, n being Element of NAT holds
( m <= n iff f . m <= f . n,S ) ) & b2 = f . k ) holds
b1 = b2
by Th2;
end;
begin
Lm4:
now for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )
let N be
with_zero set ;
for S being non empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over N holds
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )let S be non
empty with_non-empty_values IC-Ins-separated halting weakly_standard AMI-Struct over
N;
( ((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S & ( for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S)) ) )set F =
(il. (S,0)) .--> (halt S);
dom ((il. (S,0)) .--> (halt S)) = {(il. (S,0))}
by FUNCOP_1:13;
then A1:
card (dom ((il. (S,0)) .--> (halt S))) = 1
by CARD_1:30;
(il. (S,0)) .--> (halt S) is
NAT -defined the
InstructionsF of
S -valued finite lower Function
by Th25;
then A2:
LastLoc ((il. (S,0)) .--> (halt S)) =
il. (
S,
((card ((il. (S,0)) .--> (halt S))) -' 1))
by Th32
.=
il. (
S,
((card (dom ((il. (S,0)) .--> (halt S)))) -' 1))
by CARD_1:62
.=
il. (
S,
0)
by A1, XREAL_1:232
;
hence
((il. (S,0)) .--> (halt S)) . (LastLoc ((il. (S,0)) .--> (halt S))) = halt S
by FUNCOP_1:72;
for l being Element of NAT st ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) holds
l = LastLoc ((il. (S,0)) .--> (halt S))let l be
Element of
NAT ;
( ((il. (S,0)) .--> (halt S)) . l = halt S & l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )assume
((il. (S,0)) .--> (halt S)) . l = halt S
;
( l in dom ((il. (S,0)) .--> (halt S)) implies l = LastLoc ((il. (S,0)) .--> (halt S)) )assume
l in dom ((il. (S,0)) .--> (halt S))
;
l = LastLoc ((il. (S,0)) .--> (halt S))hence
l = LastLoc ((il. (S,0)) .--> (halt S))
by A2, TARSKI:def 1;
verum
end;