let V, A be set ; for loc being V -valued Function
for val being Function
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; for val being Function
for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let val be Function; for n0 being Nat st not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs holds
<*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; ( not V is empty & A is_without_nonatomicND_wrt V & loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct & loc,val are_compatible_wrt_4_locs implies <*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A)) )
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set i1 = val . 1;
set j1 = val . 2;
set n1 = val . 3;
set s1 = val . 4;
set D = ND (V,A);
set I = valid_factorial_input (V,A,val,n0);
set F = factorial_var_init (A,loc,val);
set inv = factorial_inv (A,loc,n0);
set Di = denaming (V,A,(val . 1));
set Dj = denaming (V,A,(val . 2));
set Dn = denaming (V,A,(val . 3));
set Ds = denaming (V,A,(val . 4));
set asi = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1));
set asj = SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2));
set asn = SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3));
set ass = SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4));
set S1 = SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4));
set R1 = SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3));
set Q1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2));
set P1 = SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1));
assume that
A1:
not V is empty
and
A2:
A is_without_nonatomicND_wrt V
and
A3:
loc /. 1,loc /. 2,loc /. 3,loc /. 4 are_mutually_distinct
and
A4:
loc,val are_compatible_wrt_4_locs
; <*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
A5:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A6:
<*(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A7:
<*(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
A8:
<*(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by NOMIN_3:29;
valid_factorial_input (V,A,val,n0) ||= SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))
proof
let d be
Element of
ND (
V,
A);
NOMIN_3:def 3 ( not d in dom (valid_factorial_input (V,A,val,n0)) or not (valid_factorial_input (V,A,val,n0)) . d = TRUE or ( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE ) )
assume
(
d in dom (valid_factorial_input (V,A,val,n0)) &
(valid_factorial_input (V,A,val,n0)) . d = TRUE )
;
( d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) & (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE )
then
valid_factorial_input_pred V,
A,
val,
n0,
d
by Def15;
then consider d1 being
NonatomicND of
V,
A such that A9:
d = d1
and A10:
{(val . 1),(val . 2),(val . 3),(val . 4)} c= dom d1
and A11:
d1 . (val . 1) = 0
and A12:
d1 . (val . 2) = 1
and A13:
d1 . (val . 3) = n0
and A14:
d1 . (val . 4) = 1
;
A15:
val . 1
in {(val . 1),(val . 2),(val . 3),(val . 4)}
by ENUMSET1:def 2;
A16:
val . 2
in {(val . 1),(val . 2),(val . 3),(val . 4)}
by ENUMSET1:def 2;
A17:
val . 3
in {(val . 1),(val . 2),(val . 3),(val . 4)}
by ENUMSET1:def 2;
A18:
val . 4
in {(val . 1),(val . 2),(val . 3),(val . 4)}
by ENUMSET1:def 2;
A20:
dom (denaming (V,A,(val . 1))) = { d where d is NonatomicND of V,A : val . 1 in dom d }
by NOMIN_1:def 18;
A21:
dom (denaming (V,A,(val . 2))) = { d where d is NonatomicND of V,A : val . 2 in dom d }
by NOMIN_1:def 18;
A22:
dom (denaming (V,A,(val . 3))) = { d where d is NonatomicND of V,A : val . 3 in dom d }
by NOMIN_1:def 18;
A23:
dom (denaming (V,A,(val . 4))) = { d where d is NonatomicND of V,A : val . 4 in dom d }
by NOMIN_1:def 18;
A24:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 1))) . d),(loc /. 1)) in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) & d in dom (denaming (V,A,(val . 1))) ) }
by NOMIN_2:def 11;
A25:
dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 2))) . d),(loc /. 2)) in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) & d in dom (denaming (V,A,(val . 2))) ) }
by NOMIN_2:def 11;
A26:
dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 3))) . d),(loc /. 3)) in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) & d in dom (denaming (V,A,(val . 3))) ) }
by NOMIN_2:def 11;
A27:
dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) = { d where d is TypeSCNominativeData of V,A : ( local_overlapping (V,A,d,((denaming (V,A,(val . 4))) . d),(loc /. 4)) in dom (factorial_inv (A,loc,n0)) & d in dom (denaming (V,A,(val . 4))) ) }
by NOMIN_2:def 11;
reconsider Li =
local_overlapping (
V,
A,
d1,
((denaming (V,A,(val . 1))) . d1),
(loc /. 1)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Lj =
local_overlapping (
V,
A,
Li,
((denaming (V,A,(val . 2))) . Li),
(loc /. 2)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Ln =
local_overlapping (
V,
A,
Lj,
((denaming (V,A,(val . 3))) . Lj),
(loc /. 3)) as
NonatomicND of
V,
A by NOMIN_2:9;
reconsider Ls =
local_overlapping (
V,
A,
Ln,
((denaming (V,A,(val . 4))) . Ln),
(loc /. 4)) as
NonatomicND of
V,
A by NOMIN_2:9;
A28:
d1 in dom (denaming (V,A,(val . 1)))
by A10, A15, A20;
then A29:
(denaming (V,A,(val . 1))) . d1 is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A30:
dom Li = {(loc /. 1)} \/ (dom d1)
by A1, A2, NOMIN_4:4;
dom (factorial_inv (A,loc,n0)) = ND (
V,
A)
by Def19;
then A31:
Ls in dom (factorial_inv (A,loc,n0))
;
A32:
val . 2
in dom Li
by A10, A16, A30, XBOOLE_0:def 3;
then A33:
Li in dom (denaming (V,A,(val . 2)))
by A21;
then A34:
(denaming (V,A,(val . 2))) . Li is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A35:
dom Lj = {(loc /. 2)} \/ (dom Li)
by A1, A2, NOMIN_4:4;
A36:
val . 3
in dom Li
by A10, A17, A30, XBOOLE_0:def 3;
then A37:
val . 3
in dom Lj
by A35, XBOOLE_0:def 3;
then A38:
Lj in dom (denaming (V,A,(val . 3)))
by A22;
then A39:
(denaming (V,A,(val . 3))) . Lj is
TypeSCNominativeData of
V,
A
by PARTFUN1:4, NOMIN_1:39;
then A40:
dom Ln = {(loc /. 3)} \/ (dom Lj)
by A1, A2, NOMIN_4:4;
A41:
val . 4
in dom Li
by A10, A18, A30, XBOOLE_0:def 3;
then A42:
val . 4
in dom Lj
by A35, XBOOLE_0:def 3;
then A43:
val . 4
in dom Ln
by A40, XBOOLE_0:def 3;
then A44:
Ln in dom (denaming (V,A,(val . 4)))
by A23;
then A45:
Ln in dom (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))
by A27, A31;
A46:
Lj in dom (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))
by A26, A45, A38;
then A47:
Li in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))
by A25, A33;
hence A48:
d in dom (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1)))
by A9, A24, A28;
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d = TRUE
A49:
factorial_inv_pred A,
loc,
n0,
Ls
proof
take
Ls
;
NOMIN_5:def 18 ( Ls = Ls & {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )
thus
Ls = Ls
;
( {(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls & Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )
A50:
(denaming (V,A,(val . 4))) . Ln is
TypeSCNominativeData of
V,
A
by A44, PARTFUN1:4, NOMIN_1:39;
then A51:
dom Ls = {(loc /. 4)} \/ (dom Ln)
by A1, A2, NOMIN_4:4;
loc /. 1
in {(loc /. 1)}
by TARSKI:def 1;
then A52:
loc /. 1
in dom Li
by A30, XBOOLE_0:def 3;
then A53:
loc /. 1
in dom Lj
by A35, XBOOLE_0:def 3;
then A54:
loc /. 1
in dom Ln
by A40, XBOOLE_0:def 3;
then A55:
loc /. 1
in dom Ls
by A51, XBOOLE_0:def 3;
loc /. 2
in {(loc /. 2)}
by TARSKI:def 1;
then A56:
loc /. 2
in dom Lj
by A35, XBOOLE_0:def 3;
then A57:
loc /. 2
in dom Ln
by A40, XBOOLE_0:def 3;
then A58:
loc /. 2
in dom Ls
by A51, XBOOLE_0:def 3;
loc /. 3
in {(loc /. 3)}
by TARSKI:def 1;
then A59:
loc /. 3
in dom Ln
by A40, XBOOLE_0:def 3;
then A60:
loc /. 3
in dom Ls
by A51, XBOOLE_0:def 3;
loc /. 4
in {(loc /. 4)}
by TARSKI:def 1;
then
loc /. 4
in dom Ls
by A51, XBOOLE_0:def 3;
hence
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4)} c= dom Ls
by A55, A58, A60, ENUMSET1:def 2;
( Ls . (loc /. 2) = 1 & Ls . (loc /. 3) = n0 & ex I, S being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )
thus Ls . (loc /. 2) =
Ln . (loc /. 2)
by A1, A2, A3, A50, A57, Th3
.=
Lj . (loc /. 2)
by A1, A2, A3, A39, A56, Th3
.=
(denaming (V,A,(val . 2))) . Li
by A1, A34, NOMIN_2:10
.=
denaming (
(val . 2),
Li)
by A33, NOMIN_1:def 18
.=
Li . (val . 2)
by A32, NOMIN_1:def 12
.=
1
by A1, A2, A4, A10, A16, A12, A29, Th3
;
( Ls . (loc /. 3) = n0 & ex I, S being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! ) )
thus Ls . (loc /. 3) =
Ln . (loc /. 3)
by A1, A2, A3, A50, A59, Th3
.=
(denaming (V,A,(val . 3))) . Lj
by A1, A39, NOMIN_2:10
.=
denaming (
(val . 3),
Lj)
by A38, NOMIN_1:def 18
.=
Lj . (val . 3)
by A37, NOMIN_1:def 12
.=
Li . (val . 3)
by A1, A2, A4, A34, A36, Th3
.=
n0
by A1, A2, A4, A10, A17, A13, A29, Th3
;
ex I, S being Nat st
( I = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = I ! )
A61:
Ln . (val . 4) =
Lj . (val . 4)
by A1, A2, A4, A42, A39, Th3
.=
Li . (val . 4)
by A1, A2, A4, A34, A41, Th3
.=
1
by A1, A2, A4, A10, A18, A14, A29, Th3
;
take
0
;
ex S being Nat st
( 0 = Ls . (loc /. 1) & S = Ls . (loc /. 4) & S = 0 ! )
take
1
;
( 0 = Ls . (loc /. 1) & 1 = Ls . (loc /. 4) & 1 = 0 ! )
thus Ls . (loc /. 1) =
Ln . (loc /. 1)
by A1, A2, A3, A50, A54, Th3
.=
Lj . (loc /. 1)
by A1, A2, A3, A53, A39, Th3
.=
Li . (loc /. 1)
by A1, A2, A3, A34, A52, Th3
.=
(denaming (V,A,(val . 1))) . d1
by A1, A29, NOMIN_2:10
.=
denaming (
(val . 1),
d1)
by A28, NOMIN_1:def 18
.=
0
by A10, A11, A15, NOMIN_1:def 12
;
( 1 = Ls . (loc /. 4) & 1 = 0 ! )
thus Ls . (loc /. 4) =
(denaming (V,A,(val . 4))) . Ln
by A1, A50, NOMIN_2:10
.=
denaming (
(val . 4),
Ln)
by A44, NOMIN_1:def 18
.=
1
by A61, A43, NOMIN_1:def 12
;
1 = 0 !
thus
1
= 0 !
by NEWTON:12;
verum
end;
thus (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))),(denaming (V,A,(val . 1))),(loc /. 1))) . d =
(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2))) . Li
by A9, A48, NOMIN_2:35
.=
(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))) . Lj
by A47, NOMIN_2:35
.=
(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))) . Ln
by A46, NOMIN_2:35
.=
(factorial_inv (A,loc,n0)) . Ls
by A45, NOMIN_2:35
.=
TRUE
by A31, A49, Def19
;
verum
end;
then A62:
<*(valid_factorial_input (V,A,val,n0)),(SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1))),(SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))*> is SFHT of (ND (V,A))
by A8, NOMIN_3:15;
A63:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3))),(denaming (V,A,(val . 2))),(loc /. 2)))),(SC_assignment ((denaming (V,A,(val . 2))),(loc /. 2))),(SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
A64:
<*(PP_inversion (SC_Psuperpos ((SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4))),(denaming (V,A,(val . 3))),(loc /. 3)))),(SC_assignment ((denaming (V,A,(val . 3))),(loc /. 3))),(SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
<*(PP_inversion (SC_Psuperpos ((factorial_inv (A,loc,n0)),(denaming (V,A,(val . 4))),(loc /. 4)))),(SC_assignment ((denaming (V,A,(val . 4))),(loc /. 4))),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by NOMIN_4:16;
hence
<*(valid_factorial_input (V,A,val,n0)),(factorial_var_init (A,loc,val)),(factorial_inv (A,loc,n0))*> is SFHT of (ND (V,A))
by A62, A5, A6, A7, A63, A64, Th2; verum