defpred S1[ Nat] means for p being non empty Graph-yielding FinSequence st len p = $1 & p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) holds
p . (len p) is edgeless ;
A1:
S1[1]
;
A2:
for m being non zero Nat st S1[m] holds
S1[m + 1]
proof
let m be non
zero Nat;
( S1[m] implies S1[m + 1] )
assume A3:
S1[
m]
;
S1[m + 1]
let p be non
empty Graph-yielding FinSequence;
( len p = m + 1 & p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) implies p . (len p) is edgeless )
assume that A4:
(
len p = m + 1 &
p . 1 is
edgeless )
and A5:
for
n being
Element of
dom p st
n <= (len p) - 1 holds
ex
v being
object st
p . (n + 1) is
addVertex of
p . n,
v
;
p . (len p) is edgeless
reconsider q =
p | m as non
empty Graph-yielding FinSequence ;
(m + 1) - 1
<= (len p) - 0
by A4, XREAL_1:10;
then A6:
len q = m
by FINSEQ_1:59;
A7:
1
<= m
by INT_1:74;
then A8:
q . 1 is
edgeless
by A4, FINSEQ_3:112;
now for n being Element of dom q st n <= (len q) - 1 holds
ex v being object st q . (n + 1) is addVertex of q . n,vlet n be
Element of
dom q;
( n <= (len q) - 1 implies ex v being object st q . (n + 1) is addVertex of q . n,v )assume A9:
n <= (len q) - 1
;
ex v being object st q . (n + 1) is addVertex of q . n,vthen
n + 0 <= (m - 1) + 1
by A6, XREAL_1:7;
then A10:
n <= (len p) - 1
by A4;
A11:
( 1
<= n &
n <= len q )
by FINSEQ_3:25;
then
( 1
<= n &
n + 0 <= m + 1 )
by A6, XREAL_1:7;
then reconsider k =
n as
Element of
dom p by A4, FINSEQ_3:25;
consider v being
object such that A12:
p . (k + 1) is
addVertex of
p . k,
v
by A5, A10;
take v =
v;
q . (n + 1) is addVertex of q . n,v
n + 1
<= ((len q) - 1) + 1
by A9, XREAL_1:6;
then
(
p . (k + 1) = q . (n + 1) &
p . k = q . k )
by A6, A11, FINSEQ_3:112;
hence
q . (n + 1) is
addVertex of
q . n,
v
by A12;
verum end;
then A13:
q . (len q) is
edgeless
by A3, A6, A8;
m + 0 <= ((len p) - 1) + 1
by A4, XREAL_1:6;
then reconsider k =
m as
Element of
dom p by A7, FINSEQ_3:25;
consider v being
object such that A14:
p . (k + 1) is
addVertex of
p . k,
v
by A5, A4;
p . k = q . (len q)
by A6, FINSEQ_3:112;
hence
p . (len p) is
edgeless
by A13, A4, A14;
verum
end;
A15:
for m being non zero Nat holds S1[m]
from NAT_1:sch 10(A1, A2);
let p be non empty Graph-yielding FinSequence; ( p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) implies p . (len p) is edgeless )
assume A16:
( p . 1 is edgeless & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v being object st p . (n + 1) is addVertex of p . n,v ) )
; p . (len p) is edgeless
thus
p . (len p) is edgeless
by A15, A16; verum