set a = GBP ;
let s be State of SCMPDS ; :: thesis: for f, g being FinSequence of INT
for k0, k being Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s,k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let f, g be FinSequence of INT ; :: thesis: for k0, k being Element of NAT st s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & k = s . (intpos 6) & k0 = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,k0 & g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s,k0 & len f = len g & len f > k & f is_non_decreasing_on 1,k holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,k + 1 & ( for i being Element of NAT st i > k + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= k + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= k + 1 & g . i = f . j ) ) )
let m, n be Element of NAT ; :: thesis: ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & n = s . (intpos 6) & m = ((s . (intpos 4)) - (s . (intpos 6))) - 1 & f is_FinSequence_on s,m & g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s,m & len f = len g & len f > n & f is_non_decreasing_on 1,n implies ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
assume A1: ( s . (intpos 4) >= 7 + (s . (intpos 6)) & s . GBP = 0 & n = s . (intpos 6) & m = ((s . (intpos 4)) - (s . (intpos 6))) - 1 ) ; :: thesis: ( not f is_FinSequence_on s,m or not g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s,m or not len f = len g or not len f > n or not f is_non_decreasing_on 1,n or ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
defpred S1[ Element of NAT ] means for t being State of SCMPDS
for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & $1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m & len f1 = len f2 & len f1 > $1 & f1 is_non_decreasing_on 1,$1 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,$1 + 1 & ( for i being Element of NAT st i > $1 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= $1 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= $1 + 1 & f2 . i = f1 . j ) ) );
assume A2: ( f is_FinSequence_on s,m & g is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),s,m ) ; :: thesis: ( not len f = len g or not len f > n or not f is_non_decreasing_on 1,n or ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) )
A3: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
now
let t be State of SCMPDS ; :: thesis: for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & k + 1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m & len f1 = len f2 & len f1 > k + 1 & f1 is_non_decreasing_on 1,k + 1 holds
( b4,b5 are_fiberwise_equipotent & b5 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st b6 > (k + 1) + 1 & b6 <= len b4 holds
b5 . b6 = b4 . b6 ) & ( for i being Element of NAT st 1 <= b6 & b6 <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= b7 & b7 <= (k + 1) + 1 & b5 . b6 = j . b7 ) ) )
let f1, f2 be FinSequence of INT ; :: thesis: ( t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & k + 1 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m & len f1 = len f2 & len f1 > k + 1 & f1 is_non_decreasing_on 1,k + 1 implies ( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st b4 > (k + 1) + 1 & b4 <= len b2 holds
b3 . b4 = b2 . b4 ) & ( for i being Element of NAT st 1 <= b4 & b4 <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= b5 & b5 <= (k + 1) + 1 & b3 . b4 = j . b5 ) ) ) )
assume that
A5: t . (intpos 4) >= 7 + (t . (intpos 6)) and
A6: t . GBP = 0 and
A7: k + 1 = t . (intpos 6) and
A8: m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A9: f1 is_FinSequence_on t,m and
A10: f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m and
A11: len f1 = len f2 and
A12: len f1 > k + 1 and
A13: f1 is_non_decreasing_on 1,k + 1 ; :: thesis: ( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st b4 > (k + 1) + 1 & b4 <= len b2 holds
b3 . b4 = b2 . b4 ) & ( for i being Element of NAT st 1 <= b4 & b4 <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= b5 & b5 <= (k + 1) + 1 & b3 . b4 = j . b5 ) ) )
set Bt = IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t;
set x = DataLoc (t . (intpos 4)),(- 1);
set y = DataLoc (t . (intpos 4)),0 ;
A14: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . GBP = 0 by A5, A6, A7, Lm7;
(m + 1) + (k + 1) >= 7 + (t . (intpos 6)) by A5, A7, A8;
then A15: m + 1 >= 7 by A7, XREAL_1:8;
A16: DataLoc (t . (intpos 4)),(- 1) = DataLoc m,(k + 1) by A7, A8
.= intpos (m + (k + 1)) by SCMP_GCD:5 ;
A17: ( t . (DataLoc (t . (intpos 4)),(- 1)) > t . (DataLoc (t . (intpos 4)),0 ) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (DataLoc (t . (intpos 4)),(- 1)) = t . (DataLoc (t . (intpos 4)),0 ) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (DataLoc (t . (intpos 4)),0 ) = t . (DataLoc (t . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 6) = (t . (intpos 6)) - 1 & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 4) = (t . (intpos 4)) - 1 ) ) by A5, A6, A7, Lm8;
A18: ( t . (DataLoc (t . (intpos 4)),(- 1)) <= t . (DataLoc (t . (intpos 4)),0 ) implies ( (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (DataLoc (t . (intpos 4)),(- 1)) = t . (DataLoc (t . (intpos 4)),(- 1)) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (DataLoc (t . (intpos 4)),0 ) = t . (DataLoc (t . (intpos 4)),0 ) & (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 6) = 0 ) ) by A5, A6, A7, Lm8;
A19: DataLoc (t . (intpos 4)),0 = intpos (m + (k + 2)) by A7, A8, SCMP_GCD:5;
A20: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 4) >= 7 + ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 6)) by A5, A6, A7, Lm8;
per cases ( t . (DataLoc (t . (intpos 4)),(- 1)) > t . (DataLoc (t . (intpos 4)),0 ) or t . (DataLoc (t . (intpos 4)),(- 1)) <= t . (DataLoc (t . (intpos 4)),0 ) ) ;
suppose A21: t . (DataLoc (t . (intpos 4)),(- 1)) > t . (DataLoc (t . (intpos 4)),0 ) ; :: thesis: ( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st b4 > (k + 1) + 1 & b4 <= len b2 holds
b3 . b4 = b2 . b4 ) & ( for i being Element of NAT st 1 <= b4 & b4 <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= b5 & b5 <= (k + 1) + 1 & b3 . b4 = j . b5 ) ) )
now
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len f2 implies f2 . i = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (intpos (m + i)) )
assume ( 1 <= i & i <= len f2 ) ; :: thesis: f2 . i = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (intpos (m + i))
hence f2 . i = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t) . (intpos (m + i)) by A10, Def1
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (intpos (m + i)) by A5, A6, A7, Lm15 ;
:: thesis: verum
end;
then A22: f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t),m by Def1;
A23: k + 1 < k + 2 by XREAL_1:8;
consider h being FinSequence of INT such that
A24: len h = len f1 and
A25: for i being Element of NAT st 1 <= i & i <= len h holds
h . i = (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos (m + i)) by Th2;
k + 1 > k by XREAL_1:31;
then A26: len h > k by A12, A24, XXREAL_0:2;
A27: now
let i be Element of NAT ; :: thesis: ( i <> k + 1 & i <> k + 2 & 1 <= i & i <= len f1 implies h . i = f1 . i )
assume that
A28: ( i <> k + 1 & i <> k + 2 ) and
A29: 1 <= i and
A30: i <= len f1 ; :: thesis: h . i = f1 . i
A31: ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) by A7, A8, A28;
m + i >= m + 1 by A29, XREAL_1:8;
then A32: m + i >= 7 by A15, XXREAL_0:2;
thus h . i = (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos (m + i)) by A24, A25, A29, A30
.= t . (intpos (m + i)) by A5, A6, A7, A32, A31, Lm8
.= f1 . i by A9, A29, A30, Def1 ; :: thesis: verum
end;
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= k implies h . i <= h . j )
assume that
A33: 1 <= i and
A34: i <= j and
A35: j <= k ; :: thesis: h . i <= h . j
A36: j <= len f1 by A24, A26, A35, XXREAL_0:2;
then A37: i <= len f1 by A34, XXREAL_0:2;
A38: k < k + 1 by XREAL_1:31;
then A39: j < k + 1 by A35, XXREAL_0:2;
k + 1 < (k + 1) + 1 by XREAL_1:31;
then A40: k < (k + 1) + 1 by A38, XXREAL_0:2;
j >= 1 by A33, A34, XXREAL_0:2;
then A41: h . j = f1 . j by A27, A35, A38, A40, A36;
j < k + 2 by A35, A40, XXREAL_0:2;
then h . i = f1 . i by A27, A33, A34, A39, A37;
hence h . i <= h . j by A13, A33, A34, A39, A41, GRAPH_2:def 13; :: thesis: verum
end;
then A42: h is_non_decreasing_on 1,k by GRAPH_2:def 13;
A43: len f1 >= (k + 1) + 1 by A12, INT_1:20;
A44: 1 <= k + 1 by NAT_1:11;
then A45: 1 <= k + 2 by A23, XXREAL_0:2;
then A46: h . (k + 2) = t . (DataLoc (t . (intpos 4)),(- 1)) by A19, A17, A21, A24, A25, A43;
then A47: h . (k + 2) = f1 . (k + 1) by A9, A12, A16, A44, Def1;
A48: (((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 4)) - ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos 6))) - 1 = m by A8, A17, A21;
A49: h . (k + 1) = t . (DataLoc (t . (intpos 4)),0 ) by A12, A16, A17, A21, A24, A25, NAT_1:11;
then h . (k + 1) = f1 . (k + 2) by A9, A19, A45, A43, Def1;
then A50: f1,h are_fiberwise_equipotent by A12, A24, A27, A44, A45, A43, A47, Th4;
A51: h is_FinSequence_on IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t,m by A25, Def1;
then h,f2 are_fiberwise_equipotent by A4, A7, A11, A14, A20, A17, A21, A24, A48, A22, A26, A42;
hence f1,f2 are_fiberwise_equipotent by A50, CLASSES1:84; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f2 . i = f1 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
A52: f2 is_non_decreasing_on 1,k + 1 by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42;
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f2 . b1 <= f2 . b2 )
assume that
A53: 1 <= i and
A54: i <= j and
A55: j <= (k + 1) + 1 ; :: thesis: f2 . b1 <= f2 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A55, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f2 . b1 <= f2 . b2
hence f2 . i <= f2 . j by A52, A53, A54, GRAPH_2:def 13; :: thesis: verum
end;
suppose A56: j = (k + 1) + 1 ; :: thesis: f2 . b1 <= f2 . b2
hereby :: thesis: verum
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f2 . i <= f2 . j
hence f2 . i <= f2 . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f2 . i <= f2 . j
then i < j by A54, XXREAL_0:1;
then i <= k + 1 by A56, NAT_1:13;
then consider mm being Element of NAT such that
A57: 1 <= mm and
A58: mm <= k + 1 and
A59: f2 . i = h . mm by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42, A53;
A60: f2 . j = h . (k + 2) by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42, A23, A43, A56;
hereby :: thesis: verum
per cases ( mm = k + 1 or mm <> k + 1 ) ;
suppose mm = k + 1 ; :: thesis: f2 . i <= f2 . j
hence f2 . i <= f2 . j by A12, A16, A17, A18, A24, A25, A46, A57, A59, A60; :: thesis: verum
end;
suppose A61: mm <> k + 1 ; :: thesis: f2 . i <= f2 . j
mm < k + 2 by A23, A58, XXREAL_0:2;
then mm < len h by A24, A43, XXREAL_0:2;
then A62: h . mm = f1 . mm by A24, A27, A23, A57, A58, A61;
f2 . j = f1 . (k + 1) by A9, A12, A16, A44, A46, A60, Def1;
hence f2 . i <= f2 . j by A13, A57, A58, A59, A62, GRAPH_2:def 13; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by GRAPH_2:def 13; :: thesis: ( ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f2 . i = f1 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
hereby :: thesis: for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
let i be Element of NAT ; :: thesis: ( i > (k + 1) + 1 & i <= len f1 implies f2 . i = f1 . i )
assume that
A63: i > (k + 1) + 1 and
A64: i <= len f1 ; :: thesis: f2 . i = f1 . i
A65: k + 1 < (k + 1) + 1 by XREAL_1:31;
then A66: i > k + 1 by A63, XXREAL_0:2;
1 <= k + 1 by NAT_1:11;
then A67: 1 <= i by A66, XXREAL_0:2;
thus f2 . i = h . i by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42, A64, A66
.= f1 . i by A27, A63, A64, A65, A67 ; :: thesis: verum
end;
hereby :: thesis: verum
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= (k + 1) + 1 implies ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 ) )
assume that
A68: 1 <= i and
A69: i <= (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
per cases ( i = (k + 1) + 1 or i <> (k + 1) + 1 ) ;
suppose A70: i = (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
take j = k + 1; :: thesis: ( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus 1 <= j by NAT_1:11; :: thesis: ( j <= (k + 1) + 1 & f2 . i = f1 . j )
thus j <= (k + 1) + 1 by NAT_1:11; :: thesis: f2 . i = f1 . j
thus f2 . i = f1 . j by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42, A23, A43, A47, A70; :: thesis: verum
end;
suppose i <> (k + 1) + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= b2 & b2 <= (k + 1) + 1 & f2 . j = f1 . b2 )
then i < (k + 1) + 1 by A69, XXREAL_0:1;
then i <= k + 1 by NAT_1:13;
then consider mm being Element of NAT such that
A71: 1 <= mm and
A72: mm <= k + 1 and
A73: f2 . i = h . mm by A4, A7, A11, A14, A20, A17, A21, A24, A48, A51, A22, A26, A42, A68;
hereby :: thesis: verum
A74: k + 2 = (k + 1) + 1 ;
per cases ( mm = k + 1 or mm <> k + 1 ) ;
suppose A75: mm = k + 1 ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
take j = k + 2; :: thesis: ( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus 1 <= j by A74, NAT_1:11; :: thesis: ( j <= (k + 1) + 1 & f2 . i = f1 . j )
thus j <= (k + 1) + 1 ; :: thesis: f2 . i = f1 . j
thus f2 . i = f1 . j by A9, A19, A45, A43, A49, A73, A75, Def1; :: thesis: verum
end;
suppose A76: mm <> k + 1 ; :: thesis: ex mm being Element of NAT st
( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
take mm = mm; :: thesis: ( 1 <= mm & mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus 1 <= mm by A71; :: thesis: ( mm <= (k + 1) + 1 & f2 . i = f1 . mm )
thus mm <= (k + 1) + 1 by A23, A72, XXREAL_0:2; :: thesis: f2 . i = f1 . mm
mm < k + 2 by A23, A72, XXREAL_0:2;
then mm < len f1 by A43, XXREAL_0:2;
hence f2 . i = f1 . mm by A27, A23, A71, A72, A73, A76; :: thesis: verum
end;
end;
end;
end;
end;
end;
end;
suppose A77: t . (DataLoc (t . (intpos 4)),(- 1)) <= t . (DataLoc (t . (intpos 4)),0 ) ; :: thesis: ( b2,b3 are_fiberwise_equipotent & b3 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st b4 > (k + 1) + 1 & b4 <= len b2 holds
b2 . b4 = b3 . b4 ) & ( for i being Element of NAT st 1 <= b4 & b4 <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= b5 & b5 <= (k + 1) + 1 & b3 . b4 = j . b5 ) ) )
A78: now
let i be Nat; :: thesis: ( i >= 1 & i <= len f1 implies f1 . b1 = f2 . b1 )
assume that
A79: i >= 1 and
A80: i <= len f1 ; :: thesis: f1 . b1 = f2 . b1
A81: i in NAT by ORDINAL1:def 13;
then A82: f1 . i = t . (intpos (m + i)) by A9, A79, A80, Def1;
A83: (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (DataLoc ((IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . GBP ),6) = 0 by A14, A18, A77, SCMP_GCD:5;
m + i >= m + 1 by A79, XREAL_1:8;
then A84: m + i >= 7 by A15, XXREAL_0:2;
per cases ( m + i = (t . (intpos 4)) - 1 or m + i = t . (intpos 4) or ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) ) ;
suppose A85: m + i = (t . (intpos 4)) - 1 ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (DataLoc (t . (intpos 4)),(- 1)) by A7, A8, A16, A18, A77, A82, A83, SCMPDS_8:23
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t) . (DataLoc (t . (intpos 4)),(- 1)) by A5, A6, A7, Lm15
.= f2 . i by A7, A8, A10, A11, A12, A16, A79, A85, Def1 ;
:: thesis: verum
end;
suppose A86: m + i = t . (intpos 4) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (DataLoc (t . (intpos 4)),0 ) by A7, A8, A19, A18, A77, A82, A83, SCMPDS_8:23
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t) . (DataLoc (t . (intpos 4)),0 ) by A5, A6, A7, Lm15
.= f2 . i by A7, A8, A10, A11, A19, A79, A80, A86, Def1 ;
:: thesis: verum
end;
suppose ( m + i <> (t . (intpos 4)) - 1 & m + i <> t . (intpos 4) ) ; :: thesis: f1 . b1 = f2 . b1
hence f1 . i = (IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t) . (intpos (m + i)) by A5, A6, A7, A84, A82, Lm8
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),(IExec (((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 )))),t)) . (intpos (m + i)) by A83, SCMPDS_8:23
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t) . (intpos (m + i)) by A5, A6, A7, Lm15
.= f2 . i by A10, A11, A81, A79, A80, Def1 ;
:: thesis: verum
end;
end;
end;
then A87: f1 = f2 by A11, FINSEQ_1:18;
thus f1,f2 are_fiberwise_equipotent by A11, A78, FINSEQ_1:18; :: thesis: ( f2 is_non_decreasing_on 1,(k + 1) + 1 & ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
now
let i, j be Element of NAT ; :: thesis: ( 1 <= i & i <= j & j <= (k + 1) + 1 implies f1 . b1 <= f1 . b2 )
assume that
A88: 1 <= i and
A89: i <= j and
A90: j <= (k + 1) + 1 ; :: thesis: f1 . b1 <= f1 . b2
per cases ( j <= k + 1 or j = (k + 1) + 1 ) by A90, NAT_1:8;
suppose j <= k + 1 ; :: thesis: f1 . b1 <= f1 . b2
hence f1 . i <= f1 . j by A13, A88, A89, GRAPH_2:def 13; :: thesis: verum
end;
suppose A91: j = (k + 1) + 1 ; :: thesis: f1 . b1 <= f1 . b2
hereby :: thesis: verum
per cases ( i = j or i <> j ) ;
suppose i = j ; :: thesis: f1 . i <= f1 . j
hence f1 . i <= f1 . j ; :: thesis: verum
end;
suppose i <> j ; :: thesis: f1 . i <= f1 . j
then i < j by A89, XXREAL_0:1;
then i <= k + 1 by A91, NAT_1:13;
then A92: f1 . i <= f1 . (k + 1) by A13, A88, GRAPH_2:def 13;
1 <= k + 1 by NAT_1:11;
then A93: f1 . (k + 1) = t . (DataLoc (t . (intpos 4)),(- 1)) by A9, A12, A16, Def1;
( 1 <= (k + 1) + 1 & j <= len f1 ) by A12, A91, INT_1:20, NAT_1:11;
then f1 . j = t . (DataLoc (t . (intpos 4)),0 ) by A9, A19, A91, Def1;
hence f1 . i <= f1 . j by A77, A92, A93, XXREAL_0:2; :: thesis: verum
end;
end;
end;
end;
end;
end;
hence f2 is_non_decreasing_on 1,(k + 1) + 1 by A87, GRAPH_2:def 13; :: thesis: ( ( for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) ) )
thus for i being Element of NAT st i > (k + 1) + 1 & i <= len f1 holds
f1 . i = f2 . i by A11, A78, FINSEQ_1:18; :: thesis: for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j )
thus for i being Element of NAT st 1 <= i & i <= (k + 1) + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= (k + 1) + 1 & f2 . i = f1 . j ) by A87; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A94: S1[ 0 ]
proof
let t be State of SCMPDS ; :: thesis: for f1, f2 being FinSequence of INT st t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & 0 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m & len f1 = len f2 & len f1 > 0 & f1 is_non_decreasing_on 1, 0 holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
let f1, f2 be FinSequence of INT ; :: thesis: ( t . (intpos 4) >= 7 + (t . (intpos 6)) & t . GBP = 0 & 0 = t . (intpos 6) & m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 & f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m & len f1 = len f2 & len f1 > 0 & f1 is_non_decreasing_on 1, 0 implies ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) ) )
assume that
t . (intpos 4) >= 7 + (t . (intpos 6)) and
A95: ( t . GBP = 0 & 0 = t . (intpos 6) ) and
m = ((t . (intpos 4)) - (t . (intpos 6))) - 1 and
A96: f1 is_FinSequence_on t,m and
A97: f2 is_FinSequence_on IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t,m and
A98: len f1 = len f2 and
len f1 > 0 and
f1 is_non_decreasing_on 1, 0 ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
A99: t . (DataLoc (t . GBP ),6) = 0 by A95, SCMP_GCD:5;
A100: now
let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies f1 . i = f2 . i )
assume A101: ( 1 <= i & i <= len f1 ) ; :: thesis: f1 . i = f2 . i
A102: i in NAT by ORDINAL1:def 13;
hence f1 . i = t . (intpos (m + i)) by A96, A101, Def1
.= (IExec (while>0 GBP ,6,(((GBP ,5 := (intpos 4),(- 1)) ';' (SubFrom GBP ,5,(intpos 4),0 )) ';' (if>0 GBP ,5,(((((GBP ,5 := (intpos 4),(- 1)) ';' ((intpos 4),(- 1) := (intpos 4),0 )) ';' ((intpos 4),0 := GBP ,5)) ';' (AddTo GBP ,4,(- 1))) ';' (AddTo GBP ,6,(- 1))),(Load (GBP ,6 := 0 ))))),t) . (intpos (m + i)) by A99, SCMPDS_8:23
.= f2 . i by A97, A98, A102, A101, Def1 ;
:: thesis: verum
end;
hence f1,f2 are_fiberwise_equipotent by A98, FINSEQ_1:18; :: thesis: ( f2 is_non_decreasing_on 1,0 + 1 & ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus f2 is_non_decreasing_on 1,0 + 1 by Th1; :: thesis: ( ( for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i ) & ( for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ) )
thus for i being Element of NAT st i > 0 + 1 & i <= len f1 holds
f1 . i = f2 . i by A100; :: thesis: for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j )
f1 = f2 by A98, A100, FINSEQ_1:18;
hence for i being Element of NAT st 1 <= i & i <= 0 + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= 0 + 1 & f2 . i = f1 . j ) ; :: thesis: verum
end;
A103: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A94, A3);
 assume ( len f = len g & len f > n & f is_non_decreasing_on 1,n ) ; :: thesis: ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) )
hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n + 1 & ( for i being Element of NAT st i > n + 1 & i <= len f holds
f . i = g . i ) & ( for i being Element of NAT st 1 <= i & i <= n + 1 holds
ex j being Element of NAT st
( 1 <= j & j <= n + 1 & g . i = f . j ) ) ) by A1, A2, A103; :: thesis: verum