let F, G be LTL-formula; :: thesis: ( ('not' F) . 1 = 0 & (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )
thus ('not' F) . 1 = 0 by FINSEQ_1:41; :: thesis: ( (F '&' G) . 1 = 1 & (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )
thus (F '&' G) . 1 = (<*1*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 1 by FINSEQ_1:41 ; :: thesis: ( (F 'or' G) . 1 = 2 & ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )
thus (F 'or' G) . 1 = (<*2*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 2 by FINSEQ_1:41 ; :: thesis: ( ('X' F) . 1 = 3 & (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )
thus ('X' F) . 1 = 3 by FINSEQ_1:41; :: thesis: ( (F 'U' G) . 1 = 4 & (F 'R' G) . 1 = 5 )
thus (F 'U' G) . 1 = (<*4*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 4 by FINSEQ_1:41 ; :: thesis: (F 'R' G) . 1 = 5
thus (F 'R' G) . 1 = (<*5*> ^ (F ^ G)) . 1 by FINSEQ_1:32
.= 5 by FINSEQ_1:41 ; :: thesis: verum