let V, A be set ; :: thesis: for loc being V -valued Function
for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let loc be V -valued Function; :: thesis: for x0, y0, p0, q0 being Integer
for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let x0, y0, p0, q0 be Integer; :: thesis: for n0 being Nat
for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let n0 be Nat; :: thesis: for val being 10 -element FinSequence st not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 holds
<*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
let val be 10 -element FinSequence; :: thesis: ( not V is empty & A is_without_nonatomicND_wrt V & Seg 10 c= dom loc & loc | (Seg 10) is one-to-one & loc,val are_different_wrt 10 implies <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) )
set size = 10;
set G = initial_assignments_Seq (A,loc,val,10);
A1: (initial_assignments_Seq (A,loc,val,10)) . 1 = SC_assignment ((denaming (V,A,(val . 1))),(loc /. 1)) by NOMIN_7:def 8;
set i = loc /. 1;
set j = loc /. 2;
set n = loc /. 3;
set s = loc /. 4;
set b = loc /. 5;
set c = loc /. 6;
set p = loc /. 7;
set q = loc /. 8;
set ps = loc /. 9;
set qc = loc /. 10;
set i1 = val . 1;
set j1 = val . 2;
set n1 = val . 3;
set s1 = val . 4;
set b1 = val . 5;
set c1 = val . 6;
set p1 = val . 7;
set q1 = val . 8;
set ps1 = val . 9;
set qc1 = val . 10;
set EN = {(val . 1),(val . 2),(val . 3),(val . 4),(val . 5),(val . 6),(val . 7),(val . 8),(val . 9),(val . 10)};
set D = ND (V,A);
set I = valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0);
set inv = Lucas_inv (A,loc,x0,y0,p0,q0,n0);
set DS = denamingSeq (V,A,val);
set asi = SC_assignment (((denamingSeq (V,A,val)) . 1),(loc /. 1));
set asj = SC_assignment (((denamingSeq (V,A,val)) . 2),(loc /. 2));
set asn = SC_assignment (((denamingSeq (V,A,val)) . 3),(loc /. 3));
set ass = SC_assignment (((denamingSeq (V,A,val)) . 4),(loc /. 4));
set asb = SC_assignment (((denamingSeq (V,A,val)) . 5),(loc /. 5));
set asc = SC_assignment (((denamingSeq (V,A,val)) . 6),(loc /. 6));
set asp = SC_assignment (((denamingSeq (V,A,val)) . 7),(loc /. 7));
set asq = SC_assignment (((denamingSeq (V,A,val)) . 8),(loc /. 8));
set asps = SC_assignment (((denamingSeq (V,A,val)) . 9),(loc /. 9));
set asqc = SC_assignment (((denamingSeq (V,A,val)) . 10),(loc /. 10));
set SE = SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)));
assume that
A2: not V is empty and
A3: A is_without_nonatomicND_wrt V and
A4: Seg 10 c= dom loc and
A5: loc | (Seg 10) is one-to-one and
A6: loc,val are_different_wrt 10 ; :: thesis: <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A))
A7: len val = 10 by CARD_1:def 7;
A8: len (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) = 10 by NOMIN_8:def 9, A7;
A9: len (denamingSeq (V,A,val)) = 10 by NOMIN_8:def 8, A7;
A10: ( 2 = 1 + 1 & 3 = 2 + 1 & 4 = 3 + 1 & 5 = 4 + 1 & 6 = 5 + 1 & 7 = 6 + 1 & 8 = 7 + 1 & 9 = 8 + 1 & 10 = 9 + 1 ) ;
A11: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1 = SC_Psuperpos ((Lucas_inv (A,loc,x0,y0,p0,q0,n0)),(denaming (V,A,(val . (len val)))),(loc /. (len val))) by NOMIN_8:def 9;
A12: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1),(denaming (V,A,(val . ((len val) - 1)))),(loc /. ((len val) - 1))) by A10, A8, NOMIN_8:def 9;
A13: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2),(denaming (V,A,(val . ((len val) - 2)))),(loc /. ((len val) - 2))) by A10, A8, NOMIN_8:def 9;
A14: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3),(denaming (V,A,(val . ((len val) - 3)))),(loc /. ((len val) - 3))) by A10, A8, NOMIN_8:def 9;
A15: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4),(denaming (V,A,(val . ((len val) - 4)))),(loc /. ((len val) - 4))) by A10, A8, NOMIN_8:def 9;
A16: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5),(denaming (V,A,(val . ((len val) - 5)))),(loc /. ((len val) - 5))) by A10, A8, NOMIN_8:def 9;
A17: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6),(denaming (V,A,(val . ((len val) - 6)))),(loc /. ((len val) - 6))) by A10, A8, NOMIN_8:def 9;
A18: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7),(denaming (V,A,(val . ((len val) - 7)))),(loc /. ((len val) - 7))) by A10, A8, NOMIN_8:def 9;
A19: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),(denaming (V,A,(val . ((len val) - 8)))),(loc /. ((len val) - 8))) by A10, A8, NOMIN_8:def 9;
A20: (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 10 = SC_Psuperpos (((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9),(denaming (V,A,(val . ((len val) - 9)))),(loc /. ((len val) - 9))) by A10, A8, NOMIN_8:def 9;
A21: (denamingSeq (V,A,val)) . 1 = denaming (V,A,(val . 1)) by NOMIN_8:def 8, A9;
A22: (denamingSeq (V,A,val)) . 2 = denaming (V,A,(val . 2)) by NOMIN_8:def 8, A9;
A23: (denamingSeq (V,A,val)) . 3 = denaming (V,A,(val . 3)) by NOMIN_8:def 8, A9;
A24: (denamingSeq (V,A,val)) . 4 = denaming (V,A,(val . 4)) by NOMIN_8:def 8, A9;
A25: (denamingSeq (V,A,val)) . 5 = denaming (V,A,(val . 5)) by NOMIN_8:def 8, A9;
A26: (denamingSeq (V,A,val)) . 6 = denaming (V,A,(val . 6)) by NOMIN_8:def 8, A9;
A27: (denamingSeq (V,A,val)) . 7 = denaming (V,A,(val . 7)) by NOMIN_8:def 8, A9;
A28: (denamingSeq (V,A,val)) . 8 = denaming (V,A,(val . 8)) by NOMIN_8:def 8, A9;
A29: (denamingSeq (V,A,val)) . 9 = denaming (V,A,(val . 9)) by NOMIN_8:def 8, A9;
A30: (denamingSeq (V,A,val)) . 10 = denaming (V,A,(val . 10)) by NOMIN_8:def 8, A9;
A31: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1),(SC_assignment (((denamingSeq (V,A,val)) . 10),(loc /. 10))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A7, A11, A30, NOMIN_3:29;
A32: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2),(SC_assignment (((denamingSeq (V,A,val)) . 9),(loc /. 9))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1)*> is SFHT of (ND (V,A)) by A7, A12, A29, NOMIN_3:29;
A33: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3),(SC_assignment (((denamingSeq (V,A,val)) . 8),(loc /. 8))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2)*> is SFHT of (ND (V,A)) by A7, A13, A28, NOMIN_3:29;
A34: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4),(SC_assignment (((denamingSeq (V,A,val)) . 7),(loc /. 7))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3)*> is SFHT of (ND (V,A)) by A7, A14, A27, NOMIN_3:29;
A35: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5),(SC_assignment (((denamingSeq (V,A,val)) . 6),(loc /. 6))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4)*> is SFHT of (ND (V,A)) by A7, A15, A26, NOMIN_3:29;
A36: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6),(SC_assignment (((denamingSeq (V,A,val)) . 5),(loc /. 5))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5)*> is SFHT of (ND (V,A)) by A7, A16, A25, NOMIN_3:29;
A37: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7),(SC_assignment (((denamingSeq (V,A,val)) . 4),(loc /. 4))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6)*> is SFHT of (ND (V,A)) by A7, A17, A24, NOMIN_3:29;
A38: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8),(SC_assignment (((denamingSeq (V,A,val)) . 3),(loc /. 3))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7)*> is SFHT of (ND (V,A)) by A7, A18, A23, NOMIN_3:29;
A39: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9),(SC_assignment (((denamingSeq (V,A,val)) . 2),(loc /. 2))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8)*> is SFHT of (ND (V,A)) by A7, A19, A22, NOMIN_3:29;
A40: <*((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 10),(SC_assignment (((denamingSeq (V,A,val)) . 1),(loc /. 1))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9)*> is SFHT of (ND (V,A)) by A7, A20, A21, NOMIN_3:29;
A41: (initial_assignments_Seq (A,loc,val,10)) . 2 = PP_composition ((SC_assignment (((denamingSeq (V,A,val)) . 1),(loc /. 1))),(SC_assignment (((denamingSeq (V,A,val)) . 2),(loc /. 2)))) by A10, A21, A22, A1, NOMIN_7:def 8;
A42: (initial_assignments_Seq (A,loc,val,10)) . 3 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 2),(SC_assignment (((denamingSeq (V,A,val)) . 3),(loc /. 3)))) by A10, A23, NOMIN_7:def 8;
A43: (initial_assignments_Seq (A,loc,val,10)) . 4 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 3),(SC_assignment (((denamingSeq (V,A,val)) . 4),(loc /. 4)))) by A10, A24, NOMIN_7:def 8;
A44: (initial_assignments_Seq (A,loc,val,10)) . 5 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 4),(SC_assignment (((denamingSeq (V,A,val)) . 5),(loc /. 5)))) by A10, A25, NOMIN_7:def 8;
A45: (initial_assignments_Seq (A,loc,val,10)) . 6 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 5),(SC_assignment (((denamingSeq (V,A,val)) . 6),(loc /. 6)))) by A10, A26, NOMIN_7:def 8;
A46: (initial_assignments_Seq (A,loc,val,10)) . 7 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 6),(SC_assignment (((denamingSeq (V,A,val)) . 7),(loc /. 7)))) by A10, A27, NOMIN_7:def 8;
A47: (initial_assignments_Seq (A,loc,val,10)) . 8 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 7),(SC_assignment (((denamingSeq (V,A,val)) . 8),(loc /. 8)))) by A10, A28, NOMIN_7:def 8;
A48: (initial_assignments_Seq (A,loc,val,10)) . 9 = PP_composition (((initial_assignments_Seq (A,loc,val,10)) . 8),(SC_assignment (((denamingSeq (V,A,val)) . 9),(loc /. 9)))) by A10, A29, NOMIN_7:def 8;
A49: initial_assignments (A,loc,val,10) = PP_composition ((SC_assignment (((denamingSeq (V,A,val)) . 1),(loc /. 1))),(SC_assignment (((denamingSeq (V,A,val)) . 2),(loc /. 2))),(SC_assignment (((denamingSeq (V,A,val)) . 3),(loc /. 3))),(SC_assignment (((denamingSeq (V,A,val)) . 4),(loc /. 4))),(SC_assignment (((denamingSeq (V,A,val)) . 5),(loc /. 5))),(SC_assignment (((denamingSeq (V,A,val)) . 6),(loc /. 6))),(SC_assignment (((denamingSeq (V,A,val)) . 7),(loc /. 7))),(SC_assignment (((denamingSeq (V,A,val)) . 8),(loc /. 8))),(SC_assignment (((denamingSeq (V,A,val)) . 9),(loc /. 9))),(SC_assignment (((denamingSeq (V,A,val)) . 10),(loc /. 10)))) by A10, A30, A41, A42, A43, A44, A45, A46, A47, A48, NOMIN_7:def 8;
valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0) ||= (SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 10 by A2, A3, A4, A5, A6, A8, Th13;
then A50: <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(SC_assignment (((denamingSeq (V,A,val)) . 1),(loc /. 1))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9)*> is SFHT of (ND (V,A)) by A40, NOMIN_3:15;
A51: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 9)),(SC_assignment (((denamingSeq (V,A,val)) . 2),(loc /. 2))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8)*> is SFHT of (ND (V,A)) by A7, A19, A22, NOMIN_4:16;
A52: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 8)),(SC_assignment (((denamingSeq (V,A,val)) . 3),(loc /. 3))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7)*> is SFHT of (ND (V,A)) by A7, A18, A23, NOMIN_4:16;
A53: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 7)),(SC_assignment (((denamingSeq (V,A,val)) . 4),(loc /. 4))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6)*> is SFHT of (ND (V,A)) by A7, A17, A24, NOMIN_4:16;
A54: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 6)),(SC_assignment (((denamingSeq (V,A,val)) . 5),(loc /. 5))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5)*> is SFHT of (ND (V,A)) by A7, A16, A25, NOMIN_4:16;
A55: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 5)),(SC_assignment (((denamingSeq (V,A,val)) . 6),(loc /. 6))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4)*> is SFHT of (ND (V,A)) by A7, A15, A26, NOMIN_4:16;
A56: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 4)),(SC_assignment (((denamingSeq (V,A,val)) . 7),(loc /. 7))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3)*> is SFHT of (ND (V,A)) by A7, A14, A27, NOMIN_4:16;
A57: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 3)),(SC_assignment (((denamingSeq (V,A,val)) . 8),(loc /. 8))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2)*> is SFHT of (ND (V,A)) by A7, A13, A28, NOMIN_4:16;
A58: <*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 2)),(SC_assignment (((denamingSeq (V,A,val)) . 9),(loc /. 9))),((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1)*> is SFHT of (ND (V,A)) by A7, A12, A29, NOMIN_4:16;
<*(PP_inversion ((SC_Psuperpos_Seq (loc,val,(Lucas_inv (A,loc,x0,y0,p0,q0,n0)))) . 1)),(SC_assignment (((denamingSeq (V,A,val)) . 10),(loc /. 10))),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A7, A11, A30, NOMIN_4:16;
hence <*(valid_Lucas_input (V,A,val,x0,y0,p0,q0,n0)),(initial_assignments (A,loc,val,10)),(Lucas_inv (A,loc,x0,y0,p0,q0,n0))*> is SFHT of (ND (V,A)) by A49, A32, A31, A33, A34, A35, A36, A37, A38, A39, A50, A51, A52, A53, A54, A55, A56, A57, A58, NOMIN_8:4; :: thesis: verum