set h = head phi;

set t = tail phi;

set A = I -TruthEval phi;

set B = I -TruthEval (head phi);

set C = I -TruthEval (tail phi);

set RH = (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi));

set F = S -firstChar ;

set l = (S -firstChar) . phi;

set N = TheNorSymbOf S;

((S -firstChar) . phi) \+\ (TheNorSymbOf S) = {} ;

then (S -firstChar) . phi = TheNorSymbOf S by FOMODEL0:29;

then A1: phi = (<*(TheNorSymbOf S)*> ^ (head phi)) ^ (tail phi) by Th23;

(I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi_{1} being set st b_{1} = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds

b_{1} is empty
; :: thesis: verum

set t = tail phi;

set A = I -TruthEval phi;

set B = I -TruthEval (head phi);

set C = I -TruthEval (tail phi);

set RH = (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi));

set F = S -firstChar ;

set l = (S -firstChar) . phi;

set N = TheNorSymbOf S;

((S -firstChar) . phi) \+\ (TheNorSymbOf S) = {} ;

then (S -firstChar) . phi = TheNorSymbOf S by FOMODEL0:29;

then A1: phi = (<*(TheNorSymbOf S)*> ^ (head phi)) ^ (tail phi) by Th23;

(I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

proof
end;

hence
for bper cases
( not (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 or (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 )
;

end;

suppose A2:
not (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0
; :: thesis: (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

( not I -TruthEval (head phi) = 1 & not I -TruthEval (tail phi) = 1 )
by A2;

then ( I -TruthEval (head phi) = 0 & I -TruthEval (tail phi) = 0 ) by FOMODEL0:39;

hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A1, Lm37; :: thesis: verum

end;then ( I -TruthEval (head phi) = 0 & I -TruthEval (tail phi) = 0 ) by FOMODEL0:39;

hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A1, Lm37; :: thesis: verum

suppose A3:
(I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0
; :: thesis: (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi

then
( 1 - (I -TruthEval (head phi)) = 0 or 1 - (I -TruthEval (tail phi)) = 0 )
;

then not I -TruthEval phi = 1 by A1, Lm37;

hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A3, FOMODEL0:39; :: thesis: verum

end;then not I -TruthEval phi = 1 by A1, Lm37;

hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by A3, FOMODEL0:39; :: thesis: verum

b