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 = () . phi;
set N = TheNorSymbOf S;
((S -firstChar) . phi) \+\ () = {} ;
then (S -firstChar) . phi = TheNorSymbOf S by FOMODEL0:29;
then A1: phi = (<*()*> ^ (head phi)) ^ (tail phi) by Th23;
(I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi
proof
per cases ( not (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 or (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = 0 ) ;
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 ;
hence (I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi)) = I -TruthEval phi by ; :: thesis: verum
end;
end;
end;
hence for b1 being set st b1 = (I -TruthEval phi) \+\ ((I -TruthEval (head phi)) 'nor' (I -TruthEval (tail phi))) holds
b1 is empty ; :: thesis: verum