let n be Element of NAT ; :: thesis: for p being Element of HP-WFF st p . 1 = 3 + n holds
p is simple
let p be Element of HP-WFF ; :: thesis: ( p . 1 = 3 + n implies p is simple )
assume A1: p . 1 = 3 + n ; :: thesis: p is simple
per cases ( p is conjunctive or p is conditional or p is simple or p = VERUM ) by Th9;
suppose p is conjunctive ; :: thesis: p is simple
then consider r, s being Element of HP-WFF such that
A2: p = r '&' s ;
p = <*2*> ^ (r ^ s) by A2, FINSEQ_1:32;
then 2 + 0 = 2 + (1 + n) by A1, FINSEQ_1:41;
hence p is simple ; :: thesis: verum
end;
suppose p is conditional ; :: thesis: p is simple
then consider r, s being Element of HP-WFF such that
A3: p = r => s ;
p = <*1*> ^ (r ^ s) by A3, FINSEQ_1:32;
then 1 + 0 = 1 + (2 + n) by A1, FINSEQ_1:41;
hence p is simple ; :: thesis: verum
end;
suppose p is simple ; :: thesis: p is simple
hence p is simple ; :: thesis: verum
end;
suppose p = VERUM ; :: thesis: p is simple
hence p is simple by A1, FINSEQ_1:40; :: thesis: verum
end;
end;