set WHL = while<>0 (F₅(),F₆(),F₄());
set s1 = Initialize F₂();
set P1 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set ps = ProgramPart F₂();
set sI = Initialize F₂();
set PI = F₃() +* (stop F₄());
set m1 = (LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2;
set s2 = Initialize (IExec (F₄(),F₃(),F₂()));
set P2 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set m2 = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))));
A9: stop F₄() c= F₃() +* (stop F₄()) by FUNCT_4:26;
B9: Start-At (0,SCMPDS) c= Initialize F₂() by FUNCT_4:26;
F₄() is_closed_on F₂(),F₃() by A2, A4, A5;
then A10: F₄() is_closed_on Initialize F₂(),F₃() +* (stop F₄()) by SCMPDS_6:38;
F₄() is_halting_on F₂(),F₃() by A2, A4, A5;
then A11: F₃() +* (stop F₄()) halts_on Initialize F₂() by SCMPDS_6:def 3;
F₃() +* (stop F₄()) = (F₃() +* (stop F₄())) +* (stop F₄()) by A9, FUNCT_4:104;
then (F₃() +* (stop F₄())) +* (stop F₄()) halts_on Initialize (Initialize F₂()) by A11;
then A13: F₄() is_halting_on Initialize F₂(),F₃() +* (stop F₄()) by SCMPDS_6:def 3;
set s4 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1);
set P4 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set i1 = (F₅(),F₆()) <>0_goto 2;
set i2 = goto ((card F₄()) + 2);
set i3 = goto (- ((card F₄()) + 2));
set b = DataLoc ((F₂() . F₅()),F₆());
A14: IC (Initialize F₂()) = 0 by COMPOS_1:223;
set mI = LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()));
set s5 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))));
set P5 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
set l2 = (card F₄()) + 2;
A15: while<>0 (F₅(),F₆(),F₄()) = ((F₅(),F₆()) <>0_goto 2) ';' (((goto ((card F₄()) + 2)) ';' F₄()) ';' (goto (- ((card F₄()) + 2)))) by Lm10;
set m3 = (LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1;
set s6 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1));
set P6 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
(card F₄()) + 2 < (card F₄()) + 3 by XREAL_1:8;
then A16: (card F₄()) + 2 in dom (while<>0 (F₅(),F₆(),F₄())) by Th13;
set s7 = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1));
set P7 = F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())));
A17: IExec (F₄(),F₃(),F₂()) = (Result ((F₃() +* (stop F₄())),(Initialize F₂()))) +* (F₂() | NAT) by SCMPDS_4:def 8;
A18: dom (ProgramPart F₂()) = NAT by COMPOS_1:34;
QQ: stop (while<>0 (F₅(),F₆(),F₄())) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by FUNCT_4:26;
while<>0 (F₅(),F₆(),F₄()) c= stop (while<>0 (F₅(),F₆(),F₄())) by AFINSQ_1:78;
then A19: while<>0 (F₅(),F₆(),F₄()) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by XBOOLE_1:1, QQ;
deffunc H₁( State of SCMPDS) -> Element of NAT = F₁($1);
A20: for t being State of SCMPDS st P₁[ Dstate t] & H₁( Dstate t) = 0 holds
t . (DataLoc ((F₂() . F₅()),F₆())) = 0 by A3;
A21: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = F₂() . F₅() & t . (DataLoc ((F₂() . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & H₁( Dstate (IExec (F₄(),Q,t))) < H₁( Dstate t) & P₁[ Dstate (IExec (F₄(),Q,t))] ) by A5;
A22: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(0 + 1)) = Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),0))) by EXTPRO_1:4
.= Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())) by EXTPRO_1:3
.= Exec (((F₅(),F₆()) <>0_goto 2),(Initialize F₂())) by A15, SCMPDS_6:22 ;
Shift (F₄(),2) c= while<>0 (F₅(),F₆(),F₄()) by Lm11;
then Shift (F₄(),2) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) by A19, XBOOLE_1:1;
then A23: Shift (F₄(),2) c= F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) ;

now

let a be Int_position ; :: thesis: (Initialize F₂()) . a = (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)) . a
thus (Initialize F₂()) . a = (Initialize F₂()) . a
.= (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)) . a by A22, SCMPDS_2:67 ; :: thesis: verum

end;

then A25: DataPart (Initialize F₂()) = DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)) by SCMPDS_4:23;
TT: not DataLoc ((F₂() . F₅()),F₆()) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
not F₅() in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
then (Initialize F₂()) . (DataLoc (((Initialize F₂()) . F₅()),F₆())) = (Initialize F₂()) . (DataLoc ((F₂() . F₅()),F₆())) by FUNCT_4:12
.= F₂() . (DataLoc ((F₂() . F₅()),F₆())) by TT, FUNCT_4:12 ;
then A26: IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)) = ICplusConst ((Initialize F₂()),2) by A2, A22, SCMPDS_2:67
.= 0 + 2 by A14, SCMPDS_6:23 ;
then A27: IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))))) = (card F₄()) + 2 by A1, A9, B9, A13, A10, A25, A23, SCMPDS_7:36;
A28: (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) /. (IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)))) = (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . (IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)))) by PBOOLE:158;
A29: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂())))) by EXTPRO_1:5;
then A30: CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)))) = (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2) by A1, A9, B9, A13, A10, A26, A25, A23, A28, SCMPDS_7:36
.= (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))) . ((card F₄()) + 2)
.= (while<>0 (F₅(),F₆(),F₄())) . ((card F₄()) + 2) by A16, A19, GRFUNC_1:8
.= goto (- ((card F₄()) + 2)) by Th15 ;
A32: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1)) = Following ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)))) by EXTPRO_1:4
.= Exec ((goto (- ((card F₄()) + 2))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1)))) by A30 ;
then IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1))) = ICplusConst ((Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1))),(0 - ((card F₄()) + 2))) by SCMPDS_2:66
.= 0 by A27, A29, SCMPDS_7:1 ;
then A33: IC (Initialize (IExec (F₄(),F₃(),F₂()))) = IC (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2))) by COMPOS_1:223;
A34: DataPart (Comput ((F₃() +* (stop F₄())),(Initialize F₂()),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))))) = DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))))) by A1, A9, B9, A13, A10, A26, A25, A23, SCMPDS_7:36;

now

let x be Int_position ; :: thesis: (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1))) . x = (Initialize (IExec (F₄(),F₃(),F₂()))) . x
A35: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
A36: not x in dom (F₂() | NAT) by A18, SCMPDS_2:53;
(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),1)),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))))) . x = (Comput ((F₃() +* (stop F₄())),(Initialize F₂()),(LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))))) . x by A34, SCMPDS_4:23
.= (Result ((F₃() +* (stop F₄())),(Initialize F₂()))) . x by A11, EXTPRO_1:23
.= (IExec (F₄(),F₃(),F₂())) . x by A17, A36, FUNCT_4:12 ;
hence (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1))) . x = (IExec (F₄(),F₃(),F₂())) . x by A29, A32, SCMPDS_2:66
.= (Initialize (IExec (F₄(),F₃(),F₂()))) . x by A35, FUNCT_4:12 ;
:: thesis: verum

end;

then A37: DataPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 1) + 1))) = DataPart (Initialize (IExec (F₄(),F₃(),F₂()))) by SCMPDS_4:23;
set m0 = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()));
A38: dom (ProgramPart F₂()) = (dom F₂()) /\ NAT by RELAT_1:90
.= (({(IC )} \/ SCM-Data-Loc) \/ NAT) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ;
A39: (IExec (F₄(),F₃(),F₂())) | NAT = ((Result ((F₃() +* (stop F₄())),(Initialize F₂()))) +* (ProgramPart F₂())) | NAT by SCMPDS_4:def 8
.= ProgramPart F₂() by A38, FUNCT_4:24 ;
A40: P₁[ Dstate F₂()] by A4;
( while<>0 (F₅(),F₆(),F₄()) is_closed_on F₂(),F₃() & while<>0 (F₅(),F₆(),F₄()) is_halting_on F₂(),F₃() ) from SCPINVAR:sch 3(A1, A20, A40, A21);
then A41: F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize F₂() by SCMPDS_6:def 3;
deffunc H₂( State of SCMPDS) -> Element of NAT = H₁($1);
set Es = IExec (F₄(),F₃(),F₂());
set bj = DataLoc (((IExec (F₄(),F₃(),F₂())) . F₅()),F₆());
set EP = F₃();
A42: (IExec (F₄(),F₃(),F₂())) . F₅() = F₂() . F₅() by A2, A4, A5;
then A43: for t being State of SCMPDS st P₁[ Dstate t] & H₂( Dstate t) = 0 holds
t . (DataLoc (((IExec (F₄(),F₃(),F₂())) . F₅()),F₆())) = 0 by A3;
A44: for t being State of SCMPDS
for Q being the Instructions of SCMPDS -valued ManySortedSet of NAT st P₁[ Dstate t] & t . F₅() = (IExec (F₄(),F₃(),F₂())) . F₅() & t . (DataLoc (((IExec (F₄(),F₃(),F₂())) . F₅()),F₆())) <> 0 holds
( (IExec (F₄(),Q,t)) . F₅() = t . F₅() & F₄() is_closed_on t,Q & F₄() is_halting_on t,Q & H₂( Dstate (IExec (F₄(),Q,t))) < H₂( Dstate t) & P₁[ Dstate (IExec (F₄(),Q,t))] ) by A5, A42;
A45: P₁[ Dstate (IExec (F₄(),F₃(),F₂()))] by A2, A4, A5;
( while<>0 (F₅(),F₆(),F₄()) is_closed_on IExec (F₄(),F₃(),F₂()),F₃() & while<>0 (F₅(),F₆(),F₄()) is_halting_on IExec (F₄(),F₃(),F₂()),F₃() ) from SCPINVAR:sch 3(A1, A43, A45, A44);
then A46: F₃() +* (stop (while<>0 (F₅(),F₆(),F₄()))) halts_on Initialize (IExec (F₄(),F₃(),F₂())) by SCMPDS_6:def 3;
ProgramPart (Initialize (IExec (F₄(),F₃(),F₂()))) = ProgramPart (IExec (F₄(),F₃(),F₂())) by COMPOS_1:206
.= ProgramPart ((Result ((F₃() +* (stop F₄())),(Initialize F₂()))) +* (ProgramPart F₂())) by SCMPDS_4:def 8
.= ProgramPart ((Result ((F₃() +* (stop F₄())),(Initialize F₂()))) +* (ProgramPart F₂()))
.= ProgramPart F₂() by A38, FUNCT_4:24
.= ProgramPart (Initialize F₂()) by COMPOS_1:206
.= ProgramPart (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2))) by AMI_1:123 ;
then A48: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2)) = Initialize (IExec (F₄(),F₃(),F₂())) by A37, A33, SCMPDS_7:7;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2)))) = (F₅(),F₆()) <>0_goto 2 by A15, SCMPDS_6:22;
then LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())) > (LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2 by A41, SCMPDS_6:2, SCMPDS_6:29;
then consider nn being Nat such that
A49: LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())) = ((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))))) by A48, EXTPRO_1:5;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))))) = halt SCMPDS by A46, EXTPRO_1:def 14;
then ((LifeSpan ((F₃() +* (stop F₄())),(Initialize F₂()))) + 2) + (LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))) >= LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())) by A41, EXTPRO_1:def 14;
then A51: LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) >= nn by A49, XREAL_1:8;
A52: Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂()),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())))) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),nn) by A48, A49, EXTPRO_1:5;
then CurInstr ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),nn))) = halt SCMPDS by A41, EXTPRO_1:def 14;
then nn >= LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) by A46, EXTPRO_1:def 14;
then nn = LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))) by A51, XXREAL_0:1;
then Result ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize F₂())) = Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂())))))) by A41, A52, EXTPRO_1:23;
hence IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),F₂()) = (Comput ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))),(LifeSpan ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))))) +* (ProgramPart F₂()) by SCMPDS_4:def 8
.= (Result ((F₃() +* (stop (while<>0 (F₅(),F₆(),F₄())))),(Initialize (IExec (F₄(),F₃(),F₂()))))) +* ((IExec (F₄(),F₃(),F₂())) | NAT) by A46, A39, EXTPRO_1:23
.= IExec ((while<>0 (F₅(),F₆(),F₄())),F₃(),(IExec (F₄(),F₃(),F₂()))) by SCMPDS_4:def 8 ;
:: thesis: verum