let PTN be PT_net_Str ; :: thesis:
let M0 be Boolean_marking of PTN; :: thesis:
let Q0, Q1 be FinSequence of the Transitions of PTN; :: thesis:
assume A1: Q0 ^ Q1 is_firable_on M0 ; :: thesis:

now

per cases ;

case ( Q0 = {} & Q1 = {} ) ; :: thesis:

hence ( Q1 is_firable_on Firing Q0,M0 & Q0 is_firable_on M0 ) by Def4; :: thesis:

end;

case A2: ( Q0 = {} & Q1 <> {} ) ; :: thesis:

hence Q0 is_firable_on M0 by Def4; :: thesis:
( Q0 ^ Q1 = Q1 & Firing Q0,M0 = M0 ) by A2, Def5, FINSEQ_1:47;
hence Q1 is_firable_on Firing Q0,M0 by A1; :: thesis:

end;

case A3: ( Q0 <> {} & Q1 = {} ) ; :: thesis:

hence Q1 is_firable_on Firing Q0,M0 by Def4; :: thesis:
thus Q0 is_firable_on M0 by A1, A3, FINSEQ_1:47; :: thesis:

end;

case A4: ( Q0 <> {} & Q1 <> {} ) ; :: thesis:

let i be Element of NAT ; :: thesis:
A5: len Q0 <> 0 by A4;
A6: len Q1 <> 0 by A4;
then (len Q0) + (len Q1) <> 0 by NAT_1:7;
then len (Q0 ^ Q1) <> 0 by FINSEQ_1:35;
then Q0 ^ Q1 <> {} ;
then consider M being FinSequence of Bool_marks_of PTN such that
len (Q0 ^ Q1) = len M and
A7: (Q0 ^ Q1) /. 1 is_firable_on M0 and
A8: M /. 1 = Firing ((Q0 ^ Q1) /. 1),M0 and
A9: for i being Element of NAT st i < len (Q0 ^ Q1) & i > 0 holds
( (Q0 ^ Q1) /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q0 ^ Q1) /. (i + 1)),(M /. i) ) by A1, Def4;
consider M3 being FinSequence of Bool_marks_of PTN such that
A10: len Q0 = len M3 and
A11: Firing Q0,M0 = M3 /. (len M3) and
A12: M3 /. 1 = Firing (Q0 /. 1),M0 and
A13: for i being Element of NAT st i < len Q0 & i > 0 holds
M3 /. (i + 1) = Firing (Q0 /. (i + 1)),(M3 /. i) by A4, Def5;
consider M4 being FinSequence of Bool_marks_of PTN such that
A14: len Q1 = len M4 and
Firing Q1,(Firing Q0,M0) = M4 /. (len M4) and
A15: M4 /. 1 = Firing (Q1 /. 1),(Firing Q0,M0) and
A16: for i being Element of NAT st i < len Q1 & i > 0 holds
M4 /. (i + 1) = Firing (Q1 /. (i + 1)),(M4 /. i) by A4, Def5;
A17: len Q0 > 0 by A5, NAT_1:3;
A18: len Q1 > 0 by A6, NAT_1:3;
A19: 0 + 1 <= len Q0 by A17, NAT_1:13;
defpred S₁[ Element of NAT ] means ( 1 + $1 <= len Q0 implies M /. (1 + $1) = M3 /. (1 + $1) );
A20: S₁[ 0 ] by A8, A12, Th8;
0 < len Q1 by A6, NAT_1:3;
then 0 + (len Q0) < (len Q0) + (len Q1) by XREAL_1:8;
then A21: len Q0 < len (Q0 ^ Q1) by FINSEQ_1:35;

A22: now

let k be Element of NAT ; :: thesis:
A23: 0 <= k by NAT_1:2;
then A24: 0 < 1 + k ;
assume A25: S₁[k] ; :: thesis:

now

assume A26: 1 + (k + 1) <= len Q0 ; :: thesis:
then A27: (Q0 ^ Q1) /. (1 + (k + 1)) = Q0 /. (1 + (k + 1)) by Th8, NAT_1:11;
A28: 1 + k < len Q0 by A26, NAT_1:13;
then ( 0 < 1 + k & 1 + k < len (Q0 ^ Q1) ) by A21, A23, XXREAL_0:2;
then M /. (1 + (k + 1)) = Firing (Q0 /. (1 + (k + 1))),(M3 /. (1 + k)) by A9, A25, A26, A27, NAT_1:13;
hence M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) by A13, A24, A28; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A29: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A20, A22);
A30: 0 + 1 <= len Q1 by A18, NAT_1:13;
reconsider m = (len Q0) - 1 as Element of NAT by A5, NAT_1:3, NAT_1:20;
defpred S₂[ Element of NAT ] means ( 1 + $1 <= len Q1 implies M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) );
M /. (((len Q0) + 1) + 0 ) = Firing ((Q0 ^ Q1) /. ((len Q0) + 1)),(M /. (1 + m)) by A9, A17, A21
.= Firing ((Q0 ^ Q1) /. ((len Q0) + 1)),(Firing Q0,M0) by A10, A11, A29
.= M4 /. (1 + 0 ) by A15, A30, GOBOARD2:5 ;
then A31: S₂[ 0 ] ;

A32: now

let k be Element of NAT ; :: thesis:
A33: (((len Q0) + 1) + k) + 1 = ((len Q0) + 1) + (k + 1) ;
0 <= k by NAT_1:2;
then A34: 0 < 1 + k ;
0 <= k + (len Q0) by NAT_1:2;
then A35: 0 < ((len Q0) + k) + 1 ;
assume A36: S₂[k] ; :: thesis:

now

assume A37: 1 + (k + 1) <= len Q1 ; :: thesis:
then A38: (Q0 ^ Q1) /. ((len Q0) + (1 + (k + 1))) = Q1 /. (1 + (k + 1)) by GOBOARD2:5, NAT_1:11;
A39: 1 + k < len Q1 by A37, NAT_1:13;
then (len Q0) + (1 + k) < (len Q0) + (len Q1) by XREAL_1:8;
then ((len Q0) + 1) + k < len (Q0 ^ Q1) by FINSEQ_1:35;
then M /. (((len Q0) + 1) + (k + 1)) = Firing (Q1 /. (1 + (k + 1))),(M4 /. (1 + k)) by A9, A33, A35, A36, A37, A38, NAT_1:13;
hence M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) by A16, A34, A39; :: thesis:

end;

hence S₂[k + 1] ; :: thesis:

end;

A40: for k being Element of NAT holds S₂[k] from NAT_1:sch 1(A31, A32);
consider j being Nat such that
A41: len M3 = j + 1 by A5, A10, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
len M3 = j + 1 by A41;
then A42: M /. (len M3) = M3 /. (len M3) by A10, A29;
Q1 /. 1 = (Q0 ^ Q1) /. ((len Q0) + 1) by A30, GOBOARD2:5;
then A43: Q1 /. 1 is_firable_on M3 /. (len M3) by A9, A10, A17, A21, A42;

now

let i be Element of NAT ; :: thesis:
assume A44: ( i < len Q1 & i > 0 ) ; :: thesis:
len (Q0 ^ Q1) = (len Q0) + (len Q1) by FINSEQ_1:35;
then A45: (len Q0) + i < len (Q0 ^ Q1) by A44, XREAL_1:8;
i < (len Q0) + i by A5, NAT_1:3, XREAL_1:31;
then A46: ( (Q0 ^ Q1) /. (((len Q0) + i) + 1) is_firable_on M /. ((len Q0) + i) & M /. (((len Q0) + i) + 1) = Firing ((Q0 ^ Q1) /. (((len Q0) + i) + 1)),(M /. ((len Q0) + i)) ) by A9, A44, A45;
( i + 1 >= 1 & i + 1 <= len Q1 ) by A44, NAT_1:11, NAT_1:13;
then A47: i + 1 in dom Q1 by FINSEQ_3:27;
A48: (Q0 ^ Q1) /. (((len Q0) + i) + 1) = (Q0 ^ Q1) /. ((len Q0) + (i + 1))
.= Q1 /. (i + 1) by A47, FINSEQ_4:84 ;
consider j being Nat such that
A49: i = j + 1 by A44, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
((len Q0) + 1) + j = (len Q0) + (j + 1) ;
then A50: M /. ((len Q0) + i) = M4 /. i by A40, A44, A49;
A51: ((len Q0) + 1) + i = ((len Q0) + i) + 1 ;
i + 1 <= len Q1 by A44, NAT_1:13;
hence ( Q1 /. (i + 1) is_firable_on M4 /. i & M4 /. (i + 1) = Firing (Q1 /. (i + 1)),(M4 /. i) ) by A40, A46, A48, A50, A51; :: thesis:

end;

hence Q1 is_firable_on Firing Q0,M0 by A11, A14, A15, A43, Def4; :: thesis:
A52: Q0 /. 1 is_firable_on M0 by A7, A19, Th8;

now

let i be Element of NAT ; :: thesis:
assume A53: ( i < len Q0 & i > 0 ) ; :: thesis:
then i < len (Q0 ^ Q1) by A21, XXREAL_0:2;
then A54: ( (Q0 ^ Q1) /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q0 ^ Q1) /. (i + 1)),(M /. i) ) by A9, A53;
( i + 1 >= 1 & i + 1 <= len Q0 ) by A53, NAT_1:11, NAT_1:13;
then i + 1 in dom Q0 by FINSEQ_3:27;
then A55: (Q0 ^ Q1) /. (i + 1) = Q0 /. (i + 1) by FINSEQ_4:83;
consider j being Nat such that
A56: i = j + 1 by A53, NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
i = j + 1 by A56;
then A57: M /. i = M3 /. i by A29, A53;
i + 1 <= len Q0 by A53, NAT_1:13;
hence ( Q0 /. (i + 1) is_firable_on M3 /. i & M3 /. (i + 1) = Firing (Q0 /. (i + 1)),(M3 /. i) ) by A29, A54, A55, A57; :: thesis:

end;

hence Q0 is_firable_on M0 by A10, A12, A52, Def4; :: thesis:

end;

hence ( Q1 is_firable_on Firing Q0,M0 & Q0 is_firable_on M0 ) ; :: thesis: