let p, q, r, s be Element of LTLB_WFF ; (p => (q 'or' r)) => ((r => s) => (p => (q 'or' s))) is ctaut
let g be Function of LTLB_WFF,BOOLEAN; LTLAXIO1:def 16 (VAL g) . ((p => (q 'or' r)) => ((r => s) => (p => (q 'or' s)))) = 1
set v = VAL g;
A1:
( (VAL g) . p = 1 or (VAL g) . p = 0 )
by XBOOLEAN:def 3;
A2:
( (VAL g) . r = 1 or (VAL g) . r = 0 )
by XBOOLEAN:def 3;
A3:
( (VAL g) . q = 1 or (VAL g) . q = 0 )
by XBOOLEAN:def 3;
A4: (VAL g) . ((r => s) => (p => (q 'or' s))) =
((VAL g) . (r => s)) => ((VAL g) . (p => (q 'or' s)))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((VAL g) . s)) => ((VAL g) . (p => (q 'or' s)))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((VAL g) . s)) => (((VAL g) . p) => ((VAL g) . (q 'or' s)))
by LTLAXIO1:def 15
.=
(((VAL g) . r) => ((VAL g) . s)) => (((VAL g) . p) => (((VAL g) . q) 'or' ((VAL g) . s)))
by Th5
;
A5:
( (VAL g) . s = 1 or (VAL g) . s = 0 )
by XBOOLEAN:def 3;
(VAL g) . (p => (q 'or' r)) =
((VAL g) . p) => ((VAL g) . (q 'or' r))
by LTLAXIO1:def 15
.=
((VAL g) . p) => (((VAL g) . q) 'or' ((VAL g) . r))
by Th5
;
hence (VAL g) . ((p => (q 'or' r)) => ((r => s) => (p => (q 'or' s)))) =
(((VAL g) . p) => (((VAL g) . q) 'or' ((VAL g) . r))) => ((((VAL g) . r) => ((VAL g) . s)) => (((VAL g) . p) => (((VAL g) . q) 'or' ((VAL g) . s))))
by LTLAXIO1:def 15, A4
.=
1
by A1, A2, A5, A3
;
verum