let f be non constant standard special_circular_sequence; :: thesis: for i1, j1, i2, j2 being Nat st i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent holds
( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )
let i1, j1, i2, j2 be Nat; :: thesis: ( i1 <= len (GoB f) & j1 <= width (GoB f) & i2 <= len (GoB f) & j2 <= width (GoB f) & i1,j1,i2,j2 are_adjacent implies ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) )
assume that
A1: ( i1 <= len (GoB f) & j1 <= width (GoB f) ) and
A2: i2 <= len (GoB f) and
A3: j2 <= width (GoB f) and
A4: i1,j1,i2,j2 are_adjacent ; :: thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )
A5: ( ( i1,i2 are_adjacent & j1 = j2 ) or ( i1 = i2 & j1,j2 are_adjacent ) ) by A4, GOBRD10:def 2;
now :: thesis: ( ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 & ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) & ( Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) ) ) or ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) & ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) & ( Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) implies Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) ) ) )
per cases ( ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) or ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ) by A5, GOBRD10:def 1;
case ( ( i2 = i1 + 1 or i1 = i2 + 1 ) & j1 = j2 ) ; :: thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )
hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) by A1, A2, Lm5; :: thesis: verum
end;
case ( i1 = i2 & ( j2 = j1 + 1 or j1 = j2 + 1 ) ) ; :: thesis: ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) )
hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) by A1, A3, Lm6; :: thesis: verum
end;
end;
end;
hence ( Int (cell ((GoB f),i1,j1)) c= (LeftComp f) \/ (RightComp f) iff Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f) ) ; :: thesis: verum