let F be Subset of PL-WFF; for f, f2 being FinSequence of PL-WFF
for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds
prc f2,F,i + n
let f, f2 be FinSequence of PL-WFF ; for i, n being Nat st n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i holds
prc f2,F,i + n
let i, n be Nat; ( n + (len f) <= len f2 & ( for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n) ) & 1 <= i & i <= len f & prc f,F,i implies prc f2,F,i + n )
assume that
A1:
n + (len f) <= len f2
and
A2:
for k being Nat st 1 <= k & k <= len f holds
f . k = f2 . (k + n)
and
A3:
1 <= i
and
A4:
i <= len f
; ( not prc f,F,i or prc f2,F,i + n )
i + n <= (len f) + n
by A4, XREAL_1:6;
then A5:
i + n <= len f2
by A1, XXREAL_0:2;
A6: f /. i =
f . i
by A3, A4, LTLAXIO5:1
.=
f2 . (i + n)
by A2, A3, A4
.=
f2 /. (i + n)
by A3, A5, LTLAXIO5:1, NAT_1:12
;
assume A7:
prc f,F,i
; prc f2,F,i + n
per cases
( f . i in PL_axioms or f . i in F or ex j, k being Nat st
( 1 <= j & j < i & 1 <= k & k < i & f /. j,f /. k MP_rule f /. i ) )
by A7;
suppose
ex
j,
k being
Nat st
( 1
<= j &
j < i & 1
<= k &
k < i &
f /. j,
f /. k MP_rule f /. i )
;
prc f2,F,i + nthen consider j,
k being
Nat such that A8:
1
<= j
and A9:
j < i
and A10:
1
<= k
and A11:
k < i
and A12:
f /. j,
f /. k MP_rule f /. i
;
A13:
( 1
<= j + n &
j + n < i + n )
by A8, A9, NAT_1:12, XREAL_1:8;
A14:
k <= len f
by A4, A11, XXREAL_0:2;
then
k + n <= (len f) + n
by XREAL_1:6;
then A15:
k + n <= len f2
by A1, XXREAL_0:2;
A16:
j <= len f
by A4, A9, XXREAL_0:2;
then
j + n <= (len f) + n
by XREAL_1:6;
then A17:
j + n <= len f2
by A1, XXREAL_0:2;
A18:
f /. k =
f . k
by A10, A14, LTLAXIO5:1
.=
f2 . (k + n)
by A2, A10, A14
.=
f2 /. (k + n)
by A10, A15, LTLAXIO5:1, NAT_1:12
;
A19:
( 1
<= k + n &
k + n < i + n )
by A10, A11, NAT_1:12, XREAL_1:8;
f /. j =
f . j
by A8, A16, LTLAXIO5:1
.=
f2 . (j + n)
by A2, A8, A16
.=
f2 /. (j + n)
by A8, A17, LTLAXIO5:1, NAT_1:12
;
hence
prc f2,
F,
i + n
by A6, A12, A13, A19, A18;
verum end; end;