set p1 = [0 ,0 ] .--> [1,0 ,1];
set p2 = [1,1] .--> [1,1,1];
set p3 = [1,0 ] .--> [2,1,1];
set p4 = [2,0 ] .--> [3,0 ,(- 1)];
set p5 = [2,1] .--> [3,0 ,(- 1)];
set p6 = [3,1] .--> [3,1,(- 1)];
set f = id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ;
set x1 = [0 ,0 ];
thus Succ_Tran . [0 ,0 ] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [0 ,0 ] by Th2
.= ((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) . [0 ,0 ] by Th2
.= (((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) . [0 ,0 ] by Th2
.= ((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) . [0 ,0 ] by Th2
.= (((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) . [0 ,0 ] by Th2
.= ((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) . [0 ,0 ] by Th3
.= [1,0 ,1] by FUNCT_7:96 ; :: thesis: ( Succ_Tran . [1,1] = [1,1,1] & Succ_Tran . [1,0 ] = [2,1,1] & Succ_Tran . [2,0 ] = [3,0 ,(- 1)] & Succ_Tran . [2,1] = [3,0 ,(- 1)] & Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0 ] = [4,0 ,0 ] )
set x = [1,1];
thus Succ_Tran . [1,1] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [1,1] by Th2
.= ((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) . [1,1] by Th2
.= (((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) . [1,1] by Th2
.= ((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) . [1,1] by Th2
.= (((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) . [1,1] by Th3
.= [1,1,1] by FUNCT_7:96 ; :: thesis: ( Succ_Tran . [1,0 ] = [2,1,1] & Succ_Tran . [2,0 ] = [3,0 ,(- 1)] & Succ_Tran . [2,1] = [3,0 ,(- 1)] & Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0 ] = [4,0 ,0 ] )
set x = [1,0 ];
thus Succ_Tran . [1,0 ] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [1,0 ] by Th2
.= ((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) . [1,0 ] by Th2
.= (((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) . [1,0 ] by Th2
.= ((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) . [1,0 ] by Th2
.= [2,1,1] by FUNCT_7:96 ; :: thesis: ( Succ_Tran . [2,0 ] = [3,0 ,(- 1)] & Succ_Tran . [2,1] = [3,0 ,(- 1)] & Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0 ] = [4,0 ,0 ] )
set x = [2,0 ];
thus Succ_Tran . [2,0 ] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [2,0 ] by Th2
.= ((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) . [2,0 ] by Th2
.= (((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) . [2,0 ] by Th3
.= [3,0 ,(- 1)] by FUNCT_7:96 ; :: thesis: ( Succ_Tran . [2,1] = [3,0 ,(- 1)] & Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0 ] = [4,0 ,0 ] )
set x = [2,1];
thus Succ_Tran . [2,1] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [2,1] by Th2
.= ((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) . [2,1] by Th2
.= [3,0 ,(- 1)] by FUNCT_7:96 ; :: thesis: ( Succ_Tran . [3,1] = [3,1,(- 1)] & Succ_Tran . [3,0 ] = [4,0 ,0 ] )
set x = [3,1];
thus Succ_Tran . [3,1] = (((((((id [:(SegM 4),{0 ,1}:],{(- 1),0 ,1},0 ) +* ([0 ,0 ] .--> [1,0 ,1])) +* ([1,1] .--> [1,1,1])) +* ([1,0 ] .--> [2,1,1])) +* ([2,0 ] .--> [3,0 ,(- 1)])) +* ([2,1] .--> [3,0 ,(- 1)])) +* ([3,1] .--> [3,1,(- 1)])) . [3,1] by Th3
.= [3,1,(- 1)] by FUNCT_7:96 ; :: thesis: Succ_Tran . [3,0 ] = [4,0 ,0 ]
set x = [3,0 ];
thus Succ_Tran . [3,0 ] = [4,0 ,0 ] by FUNCT_7:96; :: thesis: verum