let a be Int_position; for l being Element of NAT
for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}
let l be Element of NAT ; for k1, k2 being Integer holds NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}
let k1, k2 be Integer; NIC (((a,k1) <>0_goto k2),l) = {(l + 1),|.(k2 + l).|}
set s = the State of SCMPDS;
set i = (a,k1) <>0_goto k2;
set t = |.(k2 + l).|;
set I = (a,k1) <>0_goto k2;
reconsider n = l as Element of NAT ;
reconsider u = the n -started State of SCMPDS as Element of product (the_Values_of SCMPDS) by CARD_3:107;
let x be object ; TARSKI:def 3 ( not x in {(l + 1),|.(k2 + l).|} or x in NIC (((a,k1) <>0_goto k2),l) )
assume A6:
x in {(l + 1),|.(k2 + l).|}
; x in NIC (((a,k1) <>0_goto k2),l)
per cases
( x = l + 1 or x = |.(k2 + l).| )
by A6, TARSKI:def 2;
suppose A7:
x = l + 1
;
x in NIC (((a,k1) <>0_goto k2),l)reconsider u1 =
u +* (a .--> 0) as
State of
SCMPDS ;
reconsider u2 =
u1 +* ((DataLoc ((u1 . a),k1)) .--> 0) as
Element of
product (the_Values_of SCMPDS) by CARD_3:107;
A8:
IC u2 =
u1 . (IC )
by FUNCT_4:83, SCMPDS_2:43
.=
IC u
by FUNCT_4:83, SCMPDS_2:43
.=
n
by MEMSTR_0:def 11
;
A9:
u2 . (DataLoc ((u1 . a),k1)) = 0
by FUNCT_7:94;
u2 . (DataLoc ((u2 . a),k1)) = 0
then
x = IC (Exec (((a,k1) <>0_goto k2),u2))
by A7, A8, SCMPDS_2:55;
hence
x in NIC (
((a,k1) <>0_goto k2),
l)
by A8;
verum end; suppose A10:
x = |.(k2 + l).|
;
x in NIC (((a,k1) <>0_goto k2),l)reconsider u1 =
u +* (a .--> 1) as
State of
SCMPDS ;
reconsider u2 =
u1 +* ((DataLoc ((u1 . a),k1)) .--> 1) as
Element of
product (the_Values_of SCMPDS) by CARD_3:107;
A11:
u2 . (DataLoc ((u1 . a),k1)) = 1
by FUNCT_7:94;
A12:
u2 . (DataLoc ((u2 . a),k1)) <> 0
A13:
IC u2 =
u1 . (IC )
by FUNCT_4:83, SCMPDS_2:43
.=
IC u
by FUNCT_4:83, SCMPDS_2:43
.=
n
by MEMSTR_0:def 11
;
ex
m1 being
Element of
NAT st
(
m1 = IC u2 &
ICplusConst (
u2,
k2)
= |.(m1 + k2).| )
by SCMPDS_2:def 18;
then
x = IC (Exec (((a,k1) <>0_goto k2),u2))
by A10, A13, A12, SCMPDS_2:55;
hence
x in NIC (
((a,k1) <>0_goto k2),
l)
by A13;
verum end; end;